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

Metamath Proof Explorer

Theorem difin0ss

Description: Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994) (Proof shortened by Wolf Lammen, 30-Sep-2014)

Ref Expression
Assertion difin0ss 
|- ( ( ( A \ B ) i^i C ) = (/) -> ( C C_ A -> C C_ B ) )

Proof

Step Hyp Ref Expression
1 eq0 
 |-  ( ( ( A \ B ) i^i C ) = (/) <-> A. x -. x e. ( ( A \ B ) i^i C ) )
2 iman 
 |-  ( ( x e. C -> ( x e. A -> x e. B ) ) <-> -. ( x e. C /\ -. ( x e. A -> x e. B ) ) )
3 elin 
 |-  ( x e. ( ( A \ B ) i^i C ) <-> ( x e. ( A \ B ) /\ x e. C ) )
4 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
5 4 anbi2ci 
 |-  ( ( x e. ( A \ B ) /\ x e. C ) <-> ( x e. C /\ ( x e. A /\ -. x e. B ) ) )
6 annim 
 |-  ( ( x e. A /\ -. x e. B ) <-> -. ( x e. A -> x e. B ) )
7 6 anbi2i 
 |-  ( ( x e. C /\ ( x e. A /\ -. x e. B ) ) <-> ( x e. C /\ -. ( x e. A -> x e. B ) ) )
8 3 5 7 3bitri 
 |-  ( x e. ( ( A \ B ) i^i C ) <-> ( x e. C /\ -. ( x e. A -> x e. B ) ) )
9 2 8 xchbinxr 
 |-  ( ( x e. C -> ( x e. A -> x e. B ) ) <-> -. x e. ( ( A \ B ) i^i C ) )
10 ax-2 
 |-  ( ( x e. C -> ( x e. A -> x e. B ) ) -> ( ( x e. C -> x e. A ) -> ( x e. C -> x e. B ) ) )
11 9 10 sylbir 
 |-  ( -. x e. ( ( A \ B ) i^i C ) -> ( ( x e. C -> x e. A ) -> ( x e. C -> x e. B ) ) )
12 11 al2imi 
 |-  ( A. x -. x e. ( ( A \ B ) i^i C ) -> ( A. x ( x e. C -> x e. A ) -> A. x ( x e. C -> x e. B ) ) )
13 df-ss 
 |-  ( C C_ A <-> A. x ( x e. C -> x e. A ) )
14 df-ss 
 |-  ( C C_ B <-> A. x ( x e. C -> x e. B ) )
15 12 13 14 3imtr4g 
 |-  ( A. x -. x e. ( ( A \ B ) i^i C ) -> ( C C_ A -> C C_ B ) )
16 1 15 sylbi 
 |-  ( ( ( A \ B ) i^i C ) = (/) -> ( C C_ A -> C C_ B ) )