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

Metamath Proof Explorer

Theorem ssconb

Description: Contraposition law for subsets. (Contributed by NM, 22-Mar-1998)

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

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ C -> ( x e. A -> x e. C ) )
2 ssel 
 |-  ( B C_ C -> ( x e. B -> x e. C ) )
3 pm5.1 
 |-  ( ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) -> ( ( x e. A -> x e. C ) <-> ( x e. B -> x e. C ) ) )
4 1 2 3 syl2an 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( x e. A -> x e. C ) <-> ( x e. B -> x e. C ) ) )
5 con2b 
 |-  ( ( x e. A -> -. x e. B ) <-> ( x e. B -> -. x e. A ) )
6 5 a1i 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( x e. A -> -. x e. B ) <-> ( x e. B -> -. x e. A ) ) )
7 4 6 anbi12d 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( ( x e. A -> x e. C ) /\ ( x e. A -> -. x e. B ) ) <-> ( ( x e. B -> x e. C ) /\ ( x e. B -> -. x e. A ) ) ) )
8 jcab 
 |-  ( ( x e. A -> ( x e. C /\ -. x e. B ) ) <-> ( ( x e. A -> x e. C ) /\ ( x e. A -> -. x e. B ) ) )
9 jcab 
 |-  ( ( x e. B -> ( x e. C /\ -. x e. A ) ) <-> ( ( x e. B -> x e. C ) /\ ( x e. B -> -. x e. A ) ) )
10 7 8 9 3bitr4g 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( x e. A -> ( x e. C /\ -. x e. B ) ) <-> ( x e. B -> ( x e. C /\ -. x e. A ) ) ) )
11 eldif 
 |-  ( x e. ( C \ B ) <-> ( x e. C /\ -. x e. B ) )
12 11 imbi2i 
 |-  ( ( x e. A -> x e. ( C \ B ) ) <-> ( x e. A -> ( x e. C /\ -. x e. B ) ) )
13 eldif 
 |-  ( x e. ( C \ A ) <-> ( x e. C /\ -. x e. A ) )
14 13 imbi2i 
 |-  ( ( x e. B -> x e. ( C \ A ) ) <-> ( x e. B -> ( x e. C /\ -. x e. A ) ) )
15 10 12 14 3bitr4g 
 |-  ( ( A C_ C /\ B C_ C ) -> ( ( x e. A -> x e. ( C \ B ) ) <-> ( x e. B -> x e. ( C \ A ) ) ) )
16 15 albidv 
 |-  ( ( A C_ C /\ B C_ C ) -> ( A. x ( x e. A -> x e. ( C \ B ) ) <-> A. x ( x e. B -> x e. ( C \ A ) ) ) )
17 df-ss 
 |-  ( A C_ ( C \ B ) <-> A. x ( x e. A -> x e. ( C \ B ) ) )
18 df-ss 
 |-  ( B C_ ( C \ A ) <-> A. x ( x e. B -> x e. ( C \ A ) ) )
19 16 17 18 3bitr4g 
 |-  ( ( A C_ C /\ B C_ C ) -> ( A C_ ( C \ B ) <-> B C_ ( C \ A ) ) )