(Proof-writing)Prove $ \overline A \cup B=U \rightarrow A \subseteq B$,where A,B are sets in universe U. My proof: 
$$ \begin{array} \\ \text{1.} & \overline A \cup B =U & premise \\ 2. & x \in U \leftrightarrow(x \in A) \land x \in (\overline A \cup B) & premise \\3. &x \in A &from \ (2) \\ 4. & x \in (\overline A \cup B) \equiv \lnot(x \in A) \lor (x \in B) \equiv x \in A \rightarrow x \in B & from \ (2) \\ 5. & x \in B & mp \ from \ (3),(4) \\ 6. & A \subseteq B &from \ (3),(4),(5) \\\hline \therefore &\overline A \cup B=U \rightarrow A \subseteq B \end{array}  $$
Any critique would be helpful!
 A: Building on my comment, here's a proof. 
Suppose $\overline{A} \cup B = U$ for some universal set $U$. Let $x \in A$. Since $A \subset U$ by definition, $x \in \overline{A} \cup B$. But $x \in A$, so $x \not \in \overline{A}$. Hence, $x \in B$. Hence, $A \subset B$. 
A: The second line should be $x\in\overline A\cup B\leftrightarrow x\in U$, which is not a premise, but rather is a derivation from $1$ for an arbitrary $x$; by definition of set equality.
However you should have a premise of $A\subseteq U\wedge B\subseteq U$, since we are supposing $U$ is the universe containing $A$ and $B$.   This should perhaps be the very first thing you state.
From this premise you may derive $x\in A\to x\in U$, by definition of subset.
So when you do assume $x\in A$, you can derive $x\in\overline A\cup B$, which is $x\in\overline A\vee x\in B$ by definition of union.  
Now since $x\in A$ is equivalent to $\neg (x\in\overline A)$, you may now derive $x\in B$ under that assumption; either by a proof by cases, or using disjunctive syllogism.
Then complete the conditional proof, deducing $x\in A\to x\in B$, for arbitrary $x$, and therefore $A\subseteq B$ by definition of subset. 
A: You second line 
$x\in U \iff ( x\in A \land x\in \overline A \cup B) $
means, using distributivity and the definition of " union" by the logical operator " OR" ( symbol $\lor$)
$x\in U \iff [ (x\in A \land x\in\overline A) \lor (x\in A \land x\in B)] $
$\equiv x\in U \iff [ $ Falsity  $\lor (x\in A \land x\in B)] $
but (Falsity OR $P$) is equivalent to $P$ , so we can continue with 
$\equiv x\in U \iff [ x\in A \land x\in B] $
$\equiv A\cap B = U $
which says much more than your hypothesis $\overline A \cup B = U$. 
You may have a look at " dstributive laws" and at " identity laws" here : Catalogue of propositional logic laws
