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

Metamath Proof Explorer

Theorem r19.9rzv

Description: Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998)

		Ref	Expression
	Assertion	r19.9rzv	$⊢ A \neq \emptyset \to (φ \leftrightarrow \exists x \in A φ)$

Step	Hyp	Ref	Expression
1		dfrex2	$⊢ \exists x \in A φ \leftrightarrow \neg \forall x \in A \neg φ$
2		r19.3rzv	$⊢ A \neq \emptyset \to (\neg φ \leftrightarrow \forall x \in A \neg φ)$
3	2	con1bid	$⊢ A \neq \emptyset \to (\neg \forall x \in A \neg φ \leftrightarrow φ)$
4	1 3	bitr2id	$⊢ A \neq \emptyset \to (φ \leftrightarrow \exists x \in A φ)$