# Metamath Proof Explorer

## Theorem rexcom4

Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019)

Ref Expression
Assertion rexcom4 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 19.42v ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\left({x}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
3 2 bicomi ${⊢}\left({x}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
4 3 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
5 excom ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\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 6 bicomi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
8 7 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
9 5 8 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
10 4 9 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
11 1 10 bitri ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$