# Metamath Proof Explorer

## Theorem reeanlem

Description: Lemma factoring out common proof steps of reeanv and reean . (Contributed by Wolf Lammen, 20-Aug-2023)

Ref Expression
Hypothesis reeanlem.1 ${⊢}\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)$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 reeanlem.1 ${⊢}\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 an4 ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {B}\wedge {\psi }\right)\right)$
3 2 2exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)↔\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)$
4 3 1 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({\phi }\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)$
5 r2ex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)$
6 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
7 df-rex ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge {\psi }\right)$
8 6 7 anbi12i ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\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)$
9 4 5 8 3bitr4i ${⊢}\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)$