How to prove that if $(x \in Y) \implies (X \subset Y)$ and $(x \in Y) \lor (Y \subset X)$ , then $(X\subset Y) \lor (Y \subset X)$ I am trying to prove that if $(x \in Y) \implies (X \subset Y)$ and $(x \in Y) \lor (Y \subset X)$ , then $(X\subset Y) \lor (Y \subset X)$. 
It seems fairly obvious to me that you can effectively just replace the $(x \in Y)$ in the second hypothesis with $(X \subset Y)$, due to the first hypothesis. However, are there more steps necessary to be able to do that? And is there a name for that rule?
 A: Suppose that $X \subset Y$ doesn't hold. Then it exists $x \in X$ with $x \notin Y$. As $(x \in Y) \lor (Y \subset X)$ holds, we must have $Y \subset X$.
And if $Y \subset X$ doesn't hold, we must have $x \in Y$. Which implies using the implication $(x \in Y) \implies (X \subset Y)$ that $X \subset Y$.
Conclusion: one of $X \subset Y$ or $Y \subset X$ must hold which is the desired conslusion.
A: Essentually want to prove that $P\to Q$ and $P\vee R$ entails $Q\vee R$.
The proof will revolve around "disjunction elimination" or proof by cases.
Here's the fitch-styled natural-deduction proof:
$\begin{array}{|l}~1. ~P\to Q\quad:\textsf{Premise}\\~2.~P\vee R \quad:\textsf{Premise}\\\hline ~~\begin{array}{|l}~ 3. ~P\quad:\textsf{Assumption} \\\hline ~4.~ Q \quad:\textsf{1,3,Conditional Elimination (Modus Ponens)} \\ ~5.~Q\vee R\quad:\textsf{4,Disjunction Introduction (Weakening)} \end{array}\\~6.~P\to (Q\vee R)\quad:\textsf{3-5,Conditional Introduction}\\ ~~\begin{array}{|l} ~7.~ R\quad:\textsf{Assumption} \\\hline ~8.~ Q\vee R\quad:\textsf{7,Disjunction Introduction} \end{array}\\ ~9.~ R\to (Q\vee R)\quad:\textsf{7-8,Conditional Introduction}\\10.~ Q\vee R\quad:\textsf{2,6,9,Disjunction Elimination} \end{array}$
Just replace $P,Q,R$ by $x\in Y, X\subset Y, Y\subset X$ respectively.
