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

Metamath Proof Explorer

Theorem pssdifcom2

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

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

Proof

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