How to use of the constant " False" in a predicate logic implication appearing in a proof of : X included in EmptySet <=> X is empty

Question

While trying to prove the basic fact that : any set included in the EmptySet is empty, I was led to use the propositional constant " false" in a conditional quantified statement.

Is the following proof correct?

In case it is, what is the name of the rule allowing to go from line (3) to line (4)?

It looks like modus tollens, but is it actually? Is it , so to say, an " a fortiori" modus tollens?

Is there a basic rule saying :

from X --> f , infer ~X

(1) A is included in the EmptySet

(2) <=> for all x, x belongs to A --> x belongs to the EmptySet

(3) <=> for all x, x belongs to A ---> f

(4) <=> for all x, ~ ( x belongs to A)

(5) <=> it is false that there is an x such that x belongs to A

(6) <=> A = the EmptySet

Answer 1

It is the Negation Introduction rule.

If the Language has the falsum constant $\bot$, the rule amounts to :

$\text {from } P \to \bot, \text { derive } \lnot P$.

In fact, we can define negation from $\bot$ :

$\lnot P \leftrightarrow P \to \bot$.