# Metamath Proof Explorer

## Theorem rr19.28v

Description: Restricted quantifier version of Theorem 19.28 of Margaris p. 90. We don't need the nonempty class condition of r19.28zv when there is an outer quantifier. (Contributed by NM, 29-Oct-2012)

Ref Expression
Assertion rr19.28v ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({\phi }\wedge {\psi }\right)\to {\phi }$
2 1 ralimi ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
3 biidd ${⊢}{y}={x}\to \left({\phi }↔{\phi }\right)$
4 3 rspcv ${⊢}{x}\in {A}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }\right)$
5 2 4 syl5 ${⊢}{x}\in {A}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to {\phi }\right)$
6 simpr ${⊢}\left({\phi }\wedge {\psi }\right)\to {\psi }$
7 6 ralimi ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$
8 5 7 jca2 ${⊢}{x}\in {A}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
9 8 ralimia ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
10 r19.28v ${⊢}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$
11 10 ralimi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$
12 9 11 impbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$