Fitch Notation Set Theory

I am wanting to show that $$(A\cup B)-B\subseteq A$$ by using Fitch Notation. I think it would be as follows. Would this be correct? I am unsure as to to label the assumption step and conditional introduction. $$\def\ftc#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\ftc{}{\vdots\\\ftc{1.~(x\in A\lor x\in B)\land x\notin B\hspace{11ex}\textsf{Assumption}}{2.~(x\in A\lor x\in B)\hspace{20ex}\textsf{1, Simplification}\\3.~x\notin B\hspace{30.5ex}\textsf{1, Simplification}\\4.~x\in A\hspace{30.5ex}\textsf{2, 3, Disjunctive Sylogism}}\\5.~((x\in A\lor x\in B)\land x\notin B)\to x\in A\hspace{3.5ex}\textsf{1-4, Conditional Introduction}}$$

• Yes, that all looks correct! – Bram28 May 31 '17 at 17:47
• Is the assumption fine with the scope line without any preceding premises? That was one thing I was worried about. I apologize that it is a picture and not coded out. I would code it out, but those lines are hard to code. – W. G. May 31 '17 at 17:50
• @Bram28 I appreciate you looking at it! – W. G. May 31 '17 at 17:52
• Yes, you can start a proof with a subproof, that's fine. ... So you created this picture by hand, and not with a prover? In fact, Fitch systems typically only have INtroduction and Elimination rules, so do you have Disjunctive Syllogism available as a 1-step rule? – Bram28 May 31 '17 at 17:56
• Yes, it is a pain. What is that? As for disjunctive syllogism as a one step rule, I just use this site en.wikipedia.org/wiki/List_of_rules_of_inference – W. G. May 31 '17 at 17:57

I used variables $y$ and $z$ instead of $A$ and $B$, so this proves it for any sets $A$ and $B$, but otherwise it is exactly your proof (and, as you can see by the checkmarks, the system accepted the proof!). The $DS 2$ is Disjunctive Syllogism, proven elsewhere:
Please note though that different proof systems have different rules, so in a different system than the one I use here, the proof may look slightly different (e.g. not every system uses the explicit contradiction symbol $\bot$)