Theorem compleq

Description: Two classes are equal if and only if their complements are equal. (Contributed by BJ, 19-Mar-2021)

	Ref	Expression
Assertion	compleq	⊢ ( 𝐴 = 𝐵 ↔ ( V ∖ 𝐴 ) = ( V ∖ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		complss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( V ∖ 𝐵 ) ⊆ ( V ∖ 𝐴 ) )
2		complss	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( V ∖ 𝐴 ) ⊆ ( V ∖ 𝐵 ) )
3	1 2	anbi12ci	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ↔ ( ( V ∖ 𝐴 ) ⊆ ( V ∖ 𝐵 ) ∧ ( V ∖ 𝐵 ) ⊆ ( V ∖ 𝐴 ) ) )
4		eqss	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
5		eqss	⊢ ( ( V ∖ 𝐴 ) = ( V ∖ 𝐵 ) ↔ ( ( V ∖ 𝐴 ) ⊆ ( V ∖ 𝐵 ) ∧ ( V ∖ 𝐵 ) ⊆ ( V ∖ 𝐴 ) ) )
6	3 4 5	3bitr4i	⊢ ( 𝐴 = 𝐵 ↔ ( V ∖ 𝐴 ) = ( V ∖ 𝐵 ) )