Theorem difrab0eq

Description: If the difference between the restricting class of a restricted class abstraction and the restricted class abstraction is empty, the restricting class is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017)

	Ref	Expression
Assertion	difrab0eq	$$⊢V\setminus \left\{x\in V|\phi \right\}=\varnothing \leftrightarrow V=\left\{x\in V|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssdif0	$$⊢V\subseteq \left\{x\in V|\phi \right\}\leftrightarrow V\setminus \left\{x\in V|\phi \right\}=\varnothing$$
2		ssrabeq	$$⊢V\subseteq \left\{x\in V|\phi \right\}\leftrightarrow V=\left\{x\in V|\phi \right\}$$
3	1 2	bitr3i	$$⊢V\setminus \left\{x\in V|\phi \right\}=\varnothing \leftrightarrow V=\left\{x\in V|\phi \right\}$$