This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A = B ↔ V ∖ A = V ∖ B

Proof

Step Hyp Ref Expression
1 complss ⊢ A ⊆ B ↔ V ∖ B ⊆ V ∖ A
2 complss ⊢ B ⊆ A ↔ V ∖ A ⊆ V ∖ B
3 1 2 anbi12ci ⊢ A ⊆ B ∧ B ⊆ A ↔ V ∖ A ⊆ V ∖ B ∧ V ∖ B ⊆ V ∖ A
4 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
5 eqss ⊢ V ∖ A = V ∖ B ↔ V ∖ A ⊆ V ∖ B ∧ V ∖ B ⊆ V ∖ A
6 3 4 5 3bitr4i ⊢ A = B ↔ V ∖ A = V ∖ B