Theorem ssdifeq0

Description: A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015)

	Ref	Expression
Assertion	ssdifeq0	$$⊢A\subseteq B\setminus A\leftrightarrow A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		inidm	$$⊢A\cap A=A$$
2		ssdifin0	$$⊢A\subseteq B\setminus A\to A\cap A=\varnothing$$
3	1 2	eqtr3id	$$⊢A\subseteq B\setminus A\to A=\varnothing$$
4		0ss	$$⊢\varnothing \subseteq B\setminus \varnothing$$
5		id	$$⊢A=\varnothing \to A=\varnothing$$
6		difeq2	$$⊢A=\varnothing \to B\setminus A=B\setminus \varnothing$$
7	5 6	sseq12d	$$⊢A=\varnothing \to \left(A\subseteq B\setminus A\leftrightarrow \varnothing \subseteq B\setminus \varnothing \right)$$
8	4 7	mpbiri	$$⊢A=\varnothing \to A\subseteq B\setminus A$$
9	3 8	impbii	$$⊢A\subseteq B\setminus A\leftrightarrow A=\varnothing$$