# Metamath Proof Explorer

## Theorem rspc2ev

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999)

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

### Proof

Step Hyp Ref Expression
1 rspc2v.1 ${⊢}{x}={A}\to \left({\phi }↔{\chi }\right)$
2 rspc2v.2 ${⊢}{y}={B}\to \left({\chi }↔{\psi }\right)$
3 2 rspcev ${⊢}\left({B}\in {D}\wedge {\psi }\right)\to \exists {y}\in {D}\phantom{\rule{.4em}{0ex}}{\chi }$
4 3 anim2i ${⊢}\left({A}\in {C}\wedge \left({B}\in {D}\wedge {\psi }\right)\right)\to \left({A}\in {C}\wedge \exists {y}\in {D}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
5 4 3impb ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {\psi }\right)\to \left({A}\in {C}\wedge \exists {y}\in {D}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
6 1 rexbidv ${⊢}{x}={A}\to \left(\exists {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {D}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
7 6 rspcev ${⊢}\left({A}\in {C}\wedge \exists {y}\in {D}\phantom{\rule{.4em}{0ex}}{\chi }\right)\to \exists {x}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }$
8 5 7 syl ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {\psi }\right)\to \exists {x}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }$