This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vdif0

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

		Ref	Expression
	Assertion	vdif0	$⊢ A = V \leftrightarrow V ∖ A = \emptyset$

Step	Hyp	Ref	Expression
1		vss	$⊢ V \subseteq A \leftrightarrow A = V$
2		ssdif0	$⊢ V \subseteq A \leftrightarrow V ∖ A = \emptyset$
3	1 2	bitr3i	$⊢ A = V \leftrightarrow V ∖ A = \emptyset$