# Metamath Proof Explorer

## Theorem r19.21v

Description: Restricted quantifier version of 19.21v . (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 30-May-2011) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020)

Ref Expression
Assertion r19.21v ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\left({\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 bi2.04 ${⊢}\left({x}\in {A}\to \left({\phi }\to {\psi }\right)\right)↔\left({\phi }\to \left({x}\in {A}\to {\psi }\right)\right)$
2 1 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\phi }\to {\psi }\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({x}\in {A}\to {\psi }\right)\right)$
3 19.21v ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({x}\in {A}\to {\psi }\right)\right)↔\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\psi }\right)\right)$
4 2 3 bitri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\phi }\to {\psi }\right)\right)↔\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\psi }\right)\right)$
5 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\phi }\to {\psi }\right)\right)$
6 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\psi }\right)$
7 6 imbi2i ${⊢}\left({\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\psi }\right)\right)$
8 4 5 7 3bitr4i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\left({\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$