# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 biidd ${⊢}{y}={x}\to \left({\phi }↔{\phi }\right)$
2 1 rspcv ${⊢}{x}\in {A}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)$
3 2 ralimia ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
4 ax-1 ${⊢}{\phi }\to \left({y}\in {A}\to {\phi }\right)$
5 4 ralrimiv ${⊢}{\phi }\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
6 5 ralimi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
7 3 6 impbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$