Theorem r19.3rzv

Description: Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997) Avoid ax-12 . (Revised by TM, 16-Feb-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ax-1	$$⊢\phi \to \left(x\in A\to \phi \right)$$
2	1	ralrimiv	$$⊢\phi \to \forall x\in A\phi$$
3		rspn0	$$⊢A\ne \varnothing \to \left(\forall x\in A\phi \to \phi \right)$$
4	2 3	impbid2	$$⊢A\ne \varnothing \to \left(\phi \leftrightarrow \forall x\in A\phi \right)$$