Metamath Proof Explorer

Theorem rcompleq

Description: Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq . (Contributed by RP, 10-Jun-2021)

Ref Expression
Assertion rcompleq ⊢ A ⊆ C ∧ B ⊆ C → A = B ↔ C ∖ A = C ∖ B

Proof

Step Hyp Ref Expression
1 ancom ⊢ A ⊆ B ∧ B ⊆ A ↔ B ⊆ A ∧ A ⊆ B
2 sscon34b ⊢ B ⊆ C ∧ A ⊆ C → B ⊆ A ↔ C ∖ A ⊆ C ∖ B
3 2 ancoms ⊢ A ⊆ C ∧ B ⊆ C → B ⊆ A ↔ C ∖ A ⊆ C ∖ B
4 sscon34b ⊢ A ⊆ C ∧ B ⊆ C → A ⊆ B ↔ C ∖ B ⊆ C ∖ A
5 3 4 anbi12d ⊢ A ⊆ C ∧ B ⊆ C → B ⊆ A ∧ A ⊆ B ↔ C ∖ A ⊆ C ∖ B ∧ C ∖ B ⊆ C ∖ A
6 1 5 bitrid ⊢ A ⊆ C ∧ B ⊆ C → A ⊆ B ∧ B ⊆ A ↔ C ∖ A ⊆ C ∖ B ∧ C ∖ B ⊆ C ∖ A
7 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
8 eqss ⊢ C ∖ A = C ∖ B ↔ C ∖ A ⊆ C ∖ B ∧ C ∖ B ⊆ C ∖ A
9 6 7 8 3bitr4g ⊢ A ⊆ C ∧ B ⊆ C → A = B ↔ C ∖ A = C ∖ B