# Metamath Proof Explorer

## Theorem reeanv

Description: Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999)

Ref Expression
Assertion reeanv ${⊢}\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 exdistrv ${⊢}\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)$
2 1 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)$