Theorem r19.3rz

Description: Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008)

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

Proof

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