Metamath Proof Explorer

Theorem pssdifcom1

Description: Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 difcom 
 |-  ( ( C \ A ) C_ B <-> ( C \ B ) C_ A )
2 1 a1i 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( C \ A ) C_ B <-> ( C \ B ) C_ A ) )
3 ssconb 
 |-  ( ( B C_ C /\ A C_ C ) -> ( B C_ ( C \ A ) <-> A C_ ( C \ B ) ) )
4 3 ancoms 
 |-  ( ( A C_ C /\ B C_ C ) -> ( B C_ ( C \ A ) <-> A C_ ( C \ B ) ) )
5 4 notbid 
 |-  ( ( A C_ C /\ B C_ C ) -> ( -. B C_ ( C \ A ) <-> -. A C_ ( C \ B ) ) )
6 2 5 anbi12d 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( ( C \ A ) C_ B /\ -. B C_ ( C \ A ) ) <-> ( ( C \ B ) C_ A /\ -. A C_ ( C \ B ) ) ) )
7 dfpss3 
 |-  ( ( C \ A ) C. B <-> ( ( C \ A ) C_ B /\ -. B C_ ( C \ A ) ) )
8 dfpss3 
 |-  ( ( C \ B ) C. A <-> ( ( C \ B ) C_ A /\ -. A C_ ( C \ B ) ) )
9 6 7 8 3bitr4g 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( C \ A ) C. B <-> ( C \ B ) C. A ) )