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 B C A B C =

Proof

Step Hyp Ref Expression
1 elin x A B x A x B
2 1 imbi1i x A B x C x A x B x C
3 iman x A x B x C ¬ x A x B ¬ x C
4 2 3 bitri x A B x C ¬ x A x B ¬ x C
5 eldif x B C x B ¬ x C
6 5 anbi2i x A x B C x A x B ¬ x C
7 elin x A B C x A x B C
8 anass x A x B ¬ x C x A x B ¬ x C
9 6 7 8 3bitr4ri x A x B ¬ x C x A B C
10 4 9 xchbinx x A B x C ¬ x A B C
11 10 albii x x A B x C x ¬ x A B C
12 dfss2 A B C x x A B x C
13 eq0 A B C = x ¬ x A B C
14 11 12 13 3bitr4i A B C A B C =