# Metamath Proof Explorer

## Theorem 2rexbidva

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004)

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

### Proof

Step Hyp Ref Expression
1 2rexbidva.1 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left({\psi }↔{\chi }\right)$
2 1 anassrs ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {y}\in {B}\right)\to \left({\psi }↔{\chi }\right)$
3 2 rexbidva ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 3 rexbidva ${⊢}{\phi }\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\chi }\right)$