Theorem ssdifim

Description: Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022)

	Ref	Expression
Assertion	ssdifim	$$⊢\left(A\subseteq V\wedge B=V\setminus A\right)\to A=V\setminus B$$

Proof

Step	Hyp	Ref	Expression
1		dfss4	$$⊢A\subseteq V\leftrightarrow V\setminus \left(V\setminus A\right)=A$$
2		eqcom	$$⊢V\setminus \left(V\setminus A\right)=A\leftrightarrow A=V\setminus \left(V\setminus A\right)$$
3	1 2	sylbb	$$⊢A\subseteq V\to A=V\setminus \left(V\setminus A\right)$$
4		difeq2	$$⊢B=V\setminus A\to V\setminus B=V\setminus \left(V\setminus A\right)$$
5	4	eqcomd	$$⊢B=V\setminus A\to V\setminus \left(V\setminus A\right)=V\setminus B$$
6	3 5	sylan9eq	$$⊢\left(A\subseteq V\wedge B=V\setminus A\right)\to A=V\setminus B$$