# Metamath Proof Explorer

## Theorem rexbidv2

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999)

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

### Proof

Step Hyp Ref Expression
1 rexbidv2.1 ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {\psi }\right)↔\left({x}\in {B}\wedge {\chi }\right)\right)$
2 1 exbidv ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {\chi }\right)\right)$
3 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\psi }\right)$
4 df-rex ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {\chi }\right)$
5 2 3 4 3bitr4g ${⊢}{\phi }\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)$