Metamath Proof Explorer


Theorem ssdif0

Description: Subclass expressed in terms of difference. Exercise 7 of TakeutiZaring p. 22. (Contributed by NM, 29-Apr-1994)

Ref Expression
Assertion ssdif0 A B A B =

Proof

Step Hyp Ref Expression
1 iman x A x B ¬ x A ¬ x B
2 eldif x A B x A ¬ x B
3 1 2 xchbinxr x A x B ¬ x A B
4 3 albii x x A x B x ¬ x A B
5 dfss2 A B x x A x B
6 eq0 A B = x ¬ x A B
7 4 5 6 3bitr4i A B A B =