Theorem rr19.3v

Description: Restricted quantifier version of Theorem 19.3 of Margaris p. 89. We don't need the nonempty class condition of r19.3rzv when there is an outer quantifier. (Contributed by NM, 25-Oct-2012)

	Ref	Expression
Assertion	rr19.3v	$$⊢\forall x\in A\forall y\in A\phi \leftrightarrow \forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		biidd	$$⊢y=x\to \left(\phi \leftrightarrow \phi \right)$$
2	1	rspcv	$$⊢x\in A\to \left(\forall y\in A\phi \to \phi \right)$$
3	2	ralimia	$$⊢\forall x\in A\forall y\in A\phi \to \forall x\in A\phi$$
4		ax-1	$$⊢\phi \to \left(y\in A\to \phi \right)$$
5	4	ralrimiv	$$⊢\phi \to \forall y\in A\phi$$
6	5	ralimi	$$⊢\forall x\in A\phi \to \forall x\in A\forall y\in A\phi$$
7	3 6	impbii	$$⊢\forall x\in A\forall y\in A\phi \leftrightarrow \forall x\in A\phi$$