If the proof below proof is correct, I'd like to know what is the name of the rule involving " false" that is used here.
This question is not on " ex falso sequitur quodlibet". From false follows anything, that is clear from a semantic point of view. My question deals with the syntactic use of the propositional constant " false" and the official rules governing this use.
On
The proof seems correct.
The steps you want named are: $\quad\begin{array}{|l} x\notin B\wedge x\in B\\\bot \hspace{15ex}\text{negation elimination}\\x\in\varnothing\hspace{11ex}\text{ex falso quodlibet}\\\end{array}$
Note: some natural deduction proof systems do not have a symbol for falsum, and instead essentially incorporate the two steps into their negation elimination rule -- from a contradiction you may derive anything.
On
It all depends on what specific formal proof system you are working with and how ity is has defined its syntactic rules. In the system I use (a Fitch-style system), inferring the falsum from $P%$ and $\neg P$ is called $\bot \ Intro$, and inferring anything from a falsum is called $\bot \ Elim$
In short: yes. In particular, you're over-thinking the syntactic/semantic divide:
Remember that the syntactic side of things is supposed to reflect the semantic side of things (and vice versa for that matter, depending on which one considers "primitive"). The semantic observation is paralleled by a syntactic one - which is either an explicit rule, or derivable, in one's proof system - which allows one to syntactically infer any proposition from $\perp$. When included as an explicit rule in the system, this is often called "ex falso quodlibet," although using the same phrase for both the semantic and syntactic sides is a bit of an abuse of language.
It's worth making my first sentence below the quote precise - the key is the (strong) completeness theorem. Phrased for sequent systems, this says that "$\Gamma\vdash\varphi$" is a derivable sequent whenever every model of $\Gamma$ is also a model of $\varphi$. Since every model of $\perp$ is also a model of $\varphi$ (= semantic ex falso), completeness tells us that "$\perp$ $\vdash\varphi$" is a derivable sequent in our system.
(But the above isn't satisfying until you've seen and understood the completeness theorem so it's a bit putting the cart before the horse in this particular context.)