Theorem vdif0

Description: Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003)

	Ref	Expression
Assertion	vdif0	$$⊢A=\mathrm{V}\leftrightarrow \mathrm{V}\setminus A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		vss	$$⊢\mathrm{V}\subseteq A\leftrightarrow A=\mathrm{V}$$
2		ssdif0	$$⊢\mathrm{V}\subseteq A\leftrightarrow \mathrm{V}\setminus A=\varnothing$$
3	1 2	bitr3i	$$⊢A=\mathrm{V}\leftrightarrow \mathrm{V}\setminus A=\varnothing$$