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

Metamath Proof Explorer

Theorem sscon34b

Description: Relative complementation reverses inclusion of subclasses. Relativized version of complss . (Contributed by RP, 3-Jun-2021)

Ref Expression
Assertion sscon34b 
|- ( ( A C_ C /\ B C_ C ) -> ( A C_ B <-> ( C \ B ) C_ ( C \ A ) ) )

Proof

Step Hyp Ref Expression
1 sscon 
 |-  ( A C_ B -> ( C \ B ) C_ ( C \ A ) )
2 sscon 
 |-  ( ( C \ B ) C_ ( C \ A ) -> ( C \ ( C \ A ) ) C_ ( C \ ( C \ B ) ) )
3 dfss4 
 |-  ( A C_ C <-> ( C \ ( C \ A ) ) = A )
4 3 biimpi 
 |-  ( A C_ C -> ( C \ ( C \ A ) ) = A )
5 4 adantr 
 |-  ( ( A C_ C /\ B C_ C ) -> ( C \ ( C \ A ) ) = A )
6 dfss4 
 |-  ( B C_ C <-> ( C \ ( C \ B ) ) = B )
7 6 biimpi 
 |-  ( B C_ C -> ( C \ ( C \ B ) ) = B )
8 7 adantl 
 |-  ( ( A C_ C /\ B C_ C ) -> ( C \ ( C \ B ) ) = B )
9 5 8 sseq12d 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( C \ ( C \ A ) ) C_ ( C \ ( C \ B ) ) <-> A C_ B ) )
10 2 9 imbitrid 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( C \ B ) C_ ( C \ A ) -> A C_ B ) )
11 1 10 impbid2 
 |-  ( ( A C_ C /\ B C_ C ) -> ( A C_ B <-> ( C \ B ) C_ ( C \ A ) ) )