Theorem bj-sscon

Description: Contraposition law for relative subclasses. Relative and generalized version of ssconb , which it can shorten, as well as conss2 . (Contributed by BJ, 11-Nov-2021) This proof does not rely, even indirectly, on ssconb nor conss2 . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-sscon	⊢ ( ( 𝐴 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐵 ) ↔ ( 𝐵 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
2	1	ineq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝑉 ) = ( ( 𝐵 ∩ 𝐴 ) ∩ 𝑉 )
3	2	eqeq1i	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∩ 𝑉 ) = ∅ ↔ ( ( 𝐵 ∩ 𝐴 ) ∩ 𝑉 ) = ∅ )
4		bj-disj2r	⊢ ( ( 𝐴 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝑉 ) = ∅ )
5		bj-disj2r	⊢ ( ( 𝐵 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐴 ) ↔ ( ( 𝐵 ∩ 𝐴 ) ∩ 𝑉 ) = ∅ )
6	3 4 5	3bitr4i	⊢ ( ( 𝐴 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐵 ) ↔ ( 𝐵 ∩ 𝑉 ) ⊆ ( 𝑉 ∖ 𝐴 ) )