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

Metamath Proof Explorer

Theorem inssdif0

Description: Intersection, subclass, and difference relationship. (Contributed by NM, 27-Oct-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by Wolf Lammen, 30-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2 1 imbi1i 
 |-  ( ( x e. ( A i^i B ) -> x e. C ) <-> ( ( x e. A /\ x e. B ) -> x e. C ) )
3 iman 
 |-  ( ( ( x e. A /\ x e. B ) -> x e. C ) <-> -. ( ( x e. A /\ x e. B ) /\ -. x e. C ) )
4 2 3 bitri 
 |-  ( ( x e. ( A i^i B ) -> x e. C ) <-> -. ( ( x e. A /\ x e. B ) /\ -. x e. C ) )
5 eldif 
 |-  ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
6 5 anbi2i 
 |-  ( ( x e. A /\ x e. ( B \ C ) ) <-> ( x e. A /\ ( x e. B /\ -. x e. C ) ) )
7 elin 
 |-  ( x e. ( A i^i ( B \ C ) ) <-> ( x e. A /\ x e. ( B \ C ) ) )
8 anass 
 |-  ( ( ( x e. A /\ x e. B ) /\ -. x e. C ) <-> ( x e. A /\ ( x e. B /\ -. x e. C ) ) )
9 6 7 8 3bitr4ri 
 |-  ( ( ( x e. A /\ x e. B ) /\ -. x e. C ) <-> x e. ( A i^i ( B \ C ) ) )
10 4 9 xchbinx 
 |-  ( ( x e. ( A i^i B ) -> x e. C ) <-> -. x e. ( A i^i ( B \ C ) ) )
11 10 albii 
 |-  ( A. x ( x e. ( A i^i B ) -> x e. C ) <-> A. x -. x e. ( A i^i ( B \ C ) ) )
12 df-ss 
 |-  ( ( A i^i B ) C_ C <-> A. x ( x e. ( A i^i B ) -> x e. C ) )
13 eq0 
 |-  ( ( A i^i ( B \ C ) ) = (/) <-> A. x -. x e. ( A i^i ( B \ C ) ) )
14 11 12 13 3bitr4i 
 |-  ( ( A i^i B ) C_ C <-> ( A i^i ( B \ C ) ) = (/) )