Theorem r19.9rzv

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

	Ref	Expression
Assertion	r19.9rzv	$$⊢A\ne \varnothing \to \left(\phi \leftrightarrow \exists x\in A\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dfrex2	$$⊢\exists x\in A\phi \leftrightarrow \neg \forall x\in A\neg \phi$$
2		r19.3rzv	$$⊢A\ne \varnothing \to \left(\neg \phi \leftrightarrow \forall x\in A\neg \phi \right)$$
3	2	con1bid	$$⊢A\ne \varnothing \to \left(\neg \forall x\in A\neg \phi \leftrightarrow \phi \right)$$
4	1 3	bitr2id	$$⊢A\ne \varnothing \to \left(\phi \leftrightarrow \exists x\in A\phi \right)$$