Proof verification (formal logic): $U = \emptyset \vdash \forall A ( U \subseteq A)$ I am doing an undergrad set theory course and I want to prove this in the context of formal logic. Please criticize my attempt of proof:
$U = \emptyset \vdash\forall A ( U \subseteq A)$
Proof:
Suppose by contradiction 
$\exists A$ such that $U \nsubseteq A$. Then:
$¬ \forall x ( x \in U \rightarrow x \in A)$
$\rightarrow$ 
$...$  (I want to use material implication here. How can I write properly?)
$\rightarrow$
$\exists x (x \in U)  $
Which is a contradiction.
This may look like I am cheating, because I am trying to adapt the proof of naive set theory, and that was the hint I was given..
Any help would be appreciated.
 A: You want to prove that $\emptyset \subseteq A$ for every set $A$, i.e. that every element of $\emptyset$ is an element of $A$, for every set $A$. Let us prove that.
Let $x \in \emptyset$. By definition of $\emptyset$, such an $x$ does not exists, so we do not have anything to prove. End of the proof.
Said differently, the fact that $\emptyset \subseteq A$ for every set $A$ is vacuously true.
A: A direct proof
What we want to prove is :

$\forall a \ (\emptyset \subseteq a)$.

We have that $b \subseteq a$ is by definition : $\forall x (x \in b \to x \in a)$.
Thus, what we want to prove amounts to :

$\forall a \ [\forall x \ (x \in \emptyset \to x \in a)]$.

Now, we have the set-theory axiom : $\forall x \lnot (x \in \emptyset)$.
Now, we can "cook together the ingredients" :
1) $\forall x \lnot (x \in \emptyset)$ --- axiom
2) $\lnot (x \in \emptyset)$ --- from 1) by UI
3) $\lnot (x \in \emptyset) \to [(x \in \emptyset) \to (x \in a)]$ --- from tautology : $\lnot P \to (P \to Q)$
4) $(x \in \emptyset) \to (x \in a)$ --- from 2) and 3) by MP
5) $\forall x \ ((x \in \emptyset) \to (x \in a))$ --- from 4) by UG

6) $\forall a \ [\forall x \ ((x \in \emptyset) \to (x \in a))]$ --- from 5) by UG.


Regarding your attempt, you have assumed $\exists a \ (\emptyset \nsubseteq a)$ that means, using again the definition of $\subseteq$ :

$\exists a \ \exists x \ [(x \in \emptyset) \land (x \notin a)]$.

Using a double E-elim, we have : $(z \in \emptyset) \land (z \notin a)$, from which :

$(z \in \emptyset)$,

contradicting the axiom : $\forall x \ \lnot (x \in \emptyset)$.
