Metamath Proof Explorer

Theorem rexrab2

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis ralab2.1 ${⊢}{x}={y}\to \left({\psi }↔{\chi }\right)$
Assertion rexrab2 ${⊢}\exists {x}\in \left\{{y}\in {A}|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)$

Proof

Step Hyp Ref Expression
1 ralab2.1 ${⊢}{x}={y}\to \left({\psi }↔{\chi }\right)$
2 df-rab ${⊢}\left\{{y}\in {A}|{\phi }\right\}=\left\{{y}|\left({y}\in {A}\wedge {\phi }\right)\right\}$
3 2 rexeqi ${⊢}\exists {x}\in \left\{{y}\in {A}|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {x}\in \left\{{y}|\left({y}\in {A}\wedge {\phi }\right)\right\}\phantom{\rule{.4em}{0ex}}{\psi }$
4 1 rexab2 ${⊢}\exists {x}\in \left\{{y}|\left({y}\in {A}\wedge {\phi }\right)\right\}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {A}\wedge {\phi }\right)\wedge {\chi }\right)$
5 anass ${⊢}\left(\left({y}\in {A}\wedge {\phi }\right)\wedge {\chi }\right)↔\left({y}\in {A}\wedge \left({\phi }\wedge {\chi }\right)\right)$
6 5 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {A}\wedge {\phi }\right)\wedge {\chi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge \left({\phi }\wedge {\chi }\right)\right)$
7 df-rex ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge \left({\phi }\wedge {\chi }\right)\right)$
8 6 7 bitr4i ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {A}\wedge {\phi }\right)\wedge {\chi }\right)↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)$
9 3 4 8 3bitri ${⊢}\exists {x}\in \left\{{y}\in {A}|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)$