Theorem r19.3rzf

Description: Restricted quantification of wff not containing quantified variable. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	r19.3rzf.1	$$⊢Ⅎx\phi$$
	r19.3rzf.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	r19.3rzf	$$⊢A\ne \varnothing \to \left(\phi \leftrightarrow \forall x\in A\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		r19.3rzf.1	$$⊢Ⅎx\phi$$
2		r19.3rzf.2	$$⊢\underset{\_}{Ⅎ}xA$$
3	2	n0f	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
4		biimt	$$⊢\exists xx\in A\to \left(\phi \leftrightarrow \left(\exists xx\in A\to \phi \right)\right)$$
5	3 4	sylbi	$$⊢A\ne \varnothing \to \left(\phi \leftrightarrow \left(\exists xx\in A\to \phi \right)\right)$$
6		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
7	1	19.23	$$⊢\forall x\left(x\in A\to \phi \right)\leftrightarrow \left(\exists xx\in A\to \phi \right)$$
8	6 7	bitri	$$⊢\forall x\in A\phi \leftrightarrow \left(\exists xx\in A\to \phi \right)$$
9	5 8	bitr4di	$$⊢A\ne \varnothing \to \left(\phi \leftrightarrow \forall x\in A\phi \right)$$