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

Metamath Proof Explorer

Theorem eq0rdv

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014) Avoid ax-8 , df-clel . (Revised by GG, 6-Sep-2024)

		Ref	Expression
	Hypothesis	eq0rdv.1	$⊢ φ \to \neg x \in A$
	Assertion	eq0rdv	$⊢ φ \to A = \emptyset$

Step	Hyp	Ref	Expression
1		eq0rdv.1	$⊢ φ \to \neg x \in A$
2	1	alrimiv	$⊢ φ \to \forall x \neg x \in A$
3		eq0	$⊢ A = \emptyset \leftrightarrow \forall x \neg x \in A$
4	2 3	sylibr	$⊢ φ \to A = \emptyset$