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 C_ B <-> ( A \ B ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		iman	|- ( ( x e. A -> x e. B ) <-> -. ( x e. A /\ -. x e. B ) )
2		eldif	|- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	1 2	xchbinxr	|- ( ( x e. A -> x e. B ) <-> -. x e. ( A \ B ) )
4	3	albii	|- ( A. x ( x e. A -> x e. B ) <-> A. x -. x e. ( A \ B ) )
5		dfss2	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
6		eq0	|- ( ( A \ B ) = (/) <-> A. x -. x e. ( A \ B ) )
7	4 5 6	3bitr4i	|- ( A C_ B <-> ( A \ B ) = (/) )