Metamath Proof Explorer

Theorem sscon

Description: Contraposition law for subsets. Exercise 15 of TakeutiZaring p. 22. (Contributed by NM, 22-Mar-1998)

Ref Expression
Assertion sscon 
|- ( A C_ B -> ( C \ B ) C_ ( C \ A ) )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( x e. A -> x e. B ) )
2 1 con3d 
 |-  ( A C_ B -> ( -. x e. B -> -. x e. A ) )
3 2 anim2d 
 |-  ( A C_ B -> ( ( x e. C /\ -. x e. B ) -> ( x e. C /\ -. x e. A ) ) )
4 eldif 
 |-  ( x e. ( C \ B ) <-> ( x e. C /\ -. x e. B ) )
5 eldif 
 |-  ( x e. ( C \ A ) <-> ( x e. C /\ -. x e. A ) )
6 3 4 5 3imtr4g 
 |-  ( A C_ B -> ( x e. ( C \ B ) -> x e. ( C \ A ) ) )
7 6 ssrdv 
 |-  ( A C_ B -> ( C \ B ) C_ ( C \ A ) )