Fitch Notation Set Theory

Question

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}}$$

Answer 1

I coded it up in the Fitch prover I like to use:

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$)