Theorem bj-disj2r

Description: Relative version of ssdifin0 , allowing a biconditional, and of disj2 . (Contributed by BJ, 11-Nov-2021) This proof does not rely, even indirectly, on ssdifin0 nor disj2 . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-disj2r	$$⊢A\cap V\subseteq V\setminus B\leftrightarrow \left(A\cap B\right)\cap V=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dfss2	$$⊢A\cap V\subseteq V\setminus B\leftrightarrow \left(A\cap V\right)\cap \left(V\setminus B\right)=A\cap V$$
2		indif2	$$⊢\left(A\cap V\right)\cap \left(V\setminus B\right)=\left(\left(A\cap V\right)\cap V\right)\setminus B$$
3		inss1	$$⊢\left(A\cap V\right)\cap V\subseteq A\cap V$$
4		ssid	$$⊢A\cap V\subseteq A\cap V$$
5		inss2	$$⊢A\cap V\subseteq V$$
6	4 5	ssini	$$⊢A\cap V\subseteq \left(A\cap V\right)\cap V$$
7	3 6	eqssi	$$⊢\left(A\cap V\right)\cap V=A\cap V$$
8	7	difeq1i	$$⊢\left(\left(A\cap V\right)\cap V\right)\setminus B=\left(A\cap V\right)\setminus B$$
9	2 8	eqtri	$$⊢\left(A\cap V\right)\cap \left(V\setminus B\right)=\left(A\cap V\right)\setminus B$$
10	9	eqeq1i	$$⊢\left(A\cap V\right)\cap \left(V\setminus B\right)=A\cap V\leftrightarrow \left(A\cap V\right)\setminus B=A\cap V$$
11		eqcom	$$⊢\left(A\cap V\right)\setminus B=A\cap V\leftrightarrow A\cap V=\left(A\cap V\right)\setminus B$$
12	1 10 11	3bitri	$$⊢A\cap V\subseteq V\setminus B\leftrightarrow A\cap V=\left(A\cap V\right)\setminus B$$
13		disj3	$$⊢\left(A\cap V\right)\cap B=\varnothing \leftrightarrow A\cap V=\left(A\cap V\right)\setminus B$$
14		in32	$$⊢\left(A\cap V\right)\cap B=\left(A\cap B\right)\cap V$$
15	14	eqeq1i	$$⊢\left(A\cap V\right)\cap B=\varnothing \leftrightarrow \left(A\cap B\right)\cap V=\varnothing$$
16	12 13 15	3bitr2i	$$⊢A\cap V\subseteq V\setminus B\leftrightarrow \left(A\cap B\right)\cap V=\varnothing$$