# Metamath Proof Explorer

## Theorem r19.41v

Description: Restricted quantifier version 19.41v . Version of r19.41 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020)

Ref Expression
Assertion r19.41v ${⊢}\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 anass ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge {\psi }\right)↔\left({x}\in {A}\wedge \left({\phi }\wedge {\psi }\right)\right)$
2 1 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)$
3 19.41v ${⊢}\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)$
4 2 3 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)$
5 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)$
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 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)$
8 4 5 7 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)$