# Metamath Proof Explorer

## Theorem raaanv

Description: Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997)

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

### Proof

Step Hyp Ref Expression
1 rzal ${⊢}{A}=\varnothing \to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$
2 rzal ${⊢}{A}=\varnothing \to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
3 rzal ${⊢}{A}=\varnothing \to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$
4 pm5.1 ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
5 1 2 3 4 syl12anc ${⊢}{A}=\varnothing \to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
6 r19.28zv ${⊢}{A}\ne \varnothing \to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
7 6 ralbidv ${⊢}{A}\ne \varnothing \to \left(\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)\right)$
8 r19.27zv ${⊢}{A}\ne \varnothing \to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
9 7 8 bitrd ${⊢}{A}\ne \varnothing \to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
10 5 9 pm2.61ine ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$