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	⊢ ( ( 𝐴 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝑉 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		dfss2	⊢ ( ( 𝐴 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝑉 ) ∩ ( 𝑉 ∖ 𝐵 ) ) = ( 𝐴 ∩ 𝑉 ) )
2		indif2	⊢ ( ( 𝐴 ∩ 𝑉 ) ∩ ( 𝑉 ∖ 𝐵 ) ) = ( ( ( 𝐴 ∩ 𝑉 ) ∩ 𝑉 ) ∖ 𝐵 )
3		inss1	⊢ ( ( 𝐴 ∩ 𝑉 ) ∩ 𝑉 ) ⊆ ( 𝐴 ∩ 𝑉 )
4		ssid	⊢ ( 𝐴 ∩ 𝑉 ) ⊆ ( 𝐴 ∩ 𝑉 )
5		inss2	⊢ ( 𝐴 ∩ 𝑉 ) ⊆ 𝑉
6	4 5	ssini	⊢ ( 𝐴 ∩ 𝑉 ) ⊆ ( ( 𝐴 ∩ 𝑉 ) ∩ 𝑉 )
7	3 6	eqssi	⊢ ( ( 𝐴 ∩ 𝑉 ) ∩ 𝑉 ) = ( 𝐴 ∩ 𝑉 )
8	7	difeq1i	⊢ ( ( ( 𝐴 ∩ 𝑉 ) ∩ 𝑉 ) ∖ 𝐵 ) = ( ( 𝐴 ∩ 𝑉 ) ∖ 𝐵 )
9	2 8	eqtri	⊢ ( ( 𝐴 ∩ 𝑉 ) ∩ ( 𝑉 ∖ 𝐵 ) ) = ( ( 𝐴 ∩ 𝑉 ) ∖ 𝐵 )
10	9	eqeq1i	⊢ ( ( ( 𝐴 ∩ 𝑉 ) ∩ ( 𝑉 ∖ 𝐵 ) ) = ( 𝐴 ∩ 𝑉 ) ↔ ( ( 𝐴 ∩ 𝑉 ) ∖ 𝐵 ) = ( 𝐴 ∩ 𝑉 ) )
11		eqcom	⊢ ( ( ( 𝐴 ∩ 𝑉 ) ∖ 𝐵 ) = ( 𝐴 ∩ 𝑉 ) ↔ ( 𝐴 ∩ 𝑉 ) = ( ( 𝐴 ∩ 𝑉 ) ∖ 𝐵 ) )
12	1 10 11	3bitri	⊢ ( ( 𝐴 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐵 ) ↔ ( 𝐴 ∩ 𝑉 ) = ( ( 𝐴 ∩ 𝑉 ) ∖ 𝐵 ) )
13		disj3	⊢ ( ( ( 𝐴 ∩ 𝑉 ) ∩ 𝐵 ) = ∅ ↔ ( 𝐴 ∩ 𝑉 ) = ( ( 𝐴 ∩ 𝑉 ) ∖ 𝐵 ) )
14		in32	⊢ ( ( 𝐴 ∩ 𝑉 ) ∩ 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∩ 𝑉 )
15	14	eqeq1i	⊢ ( ( ( 𝐴 ∩ 𝑉 ) ∩ 𝐵 ) = ∅ ↔ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝑉 ) = ∅ )
16	12 13 15	3bitr2i	⊢ ( ( 𝐴 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝑉 ) = ∅ )