Theorem r19.3rzv

Description: Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997)

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

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎx\phi$$
2	1	r19.3rz	$$⊢A\ne \varnothing \to \left(\phi \leftrightarrow \forall x\in A\phi \right)$$