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

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_ C /\ B C_ C ) -> ( A = B <-> ( C \ A ) = ( C \ B ) ) )

Proof

Step Hyp Ref Expression
1 ancom 
 |-  ( ( A C_ B /\ B C_ A ) <-> ( B C_ A /\ A C_ B ) )
2 sscon34b 
 |-  ( ( B C_ C /\ A C_ C ) -> ( B C_ A <-> ( C \ A ) C_ ( C \ B ) ) )
3 2 ancoms 
 |-  ( ( A C_ C /\ B C_ C ) -> ( B C_ A <-> ( C \ A ) C_ ( C \ B ) ) )
4 sscon34b 
 |-  ( ( A C_ C /\ B C_ C ) -> ( A C_ B <-> ( C \ B ) C_ ( C \ A ) ) )
5 3 4 anbi12d 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( B C_ A /\ A C_ B ) <-> ( ( C \ A ) C_ ( C \ B ) /\ ( C \ B ) C_ ( C \ A ) ) ) )
6 1 5 bitrid 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( A C_ B /\ B C_ A ) <-> ( ( C \ A ) C_ ( C \ B ) /\ ( C \ B ) C_ ( C \ A ) ) ) )
7 eqss 
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
8 eqss 
 |-  ( ( C \ A ) = ( C \ B ) <-> ( ( C \ A ) C_ ( C \ B ) /\ ( C \ B ) C_ ( C \ A ) ) )
9 6 7 8 3bitr4g 
 |-  ( ( A C_ C /\ B C_ C ) -> ( A = B <-> ( C \ A ) = ( C \ B ) ) )