# Metamath Proof Explorer

## Theorem reean

Description: Rearrange restricted existential quantifiers. (Contributed by NM, 27-Oct-2010) (Proof shortened by Andrew Salmon, 30-May-2011)

Ref Expression
Hypotheses reean.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
reean.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion reean ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 reean.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 reean.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
4 3 1 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
5 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
6 5 2 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {\psi }\right)$
7 4 6 eean ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {B}\wedge {\psi }\right)\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {\psi }\right)\right)$
8 7 reeanlem ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)$