# Metamath Proof Explorer

## Theorem r19.41

Description: Restricted quantifier version of 19.41 . See r19.41v for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010)

Ref Expression
Hypothesis r19.41.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion r19.41 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 r19.41.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
2 anass ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {\psi }\right)↔\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)$
3 2 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)$
4 1 19.41 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\wedge {\psi }\right)$
5 3 4 bitr3i ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\wedge {\psi }\right)$
6 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)$
7 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
8 7 anbi1i ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\wedge {\psi }\right)$
9 5 6 8 3bitr4i ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)$