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 ) ) = (/) )