Theorem vdif0

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

	Ref	Expression
Assertion	vdif0	⊢ ( 𝐴 = V ↔ ( V ∖ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		vss	⊢ ( V ⊆ 𝐴 ↔ 𝐴 = V )
2		ssdif0	⊢ ( V ⊆ 𝐴 ↔ ( V ∖ 𝐴 ) = ∅ )
3	1 2	bitr3i	⊢ ( 𝐴 = V ↔ ( V ∖ 𝐴 ) = ∅ )