# Metamath Proof Explorer

## Theorem spc2egv

Description: Existential specialization with two quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995)

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

### Proof

Step Hyp Ref Expression
1 spc2egv.1 ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left({\phi }↔{\psi }\right)$
2 elisset ${⊢}{A}\in {V}\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
3 elisset ${⊢}{B}\in {W}\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}={B}$
4 2 3 anim12i ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{y}={B}\right)$
5 exdistrv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {y}={B}\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{y}={B}\right)$
6 4 5 sylibr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {y}={B}\right)$
7 1 biimprcd ${⊢}{\psi }\to \left(\left({x}={A}\wedge {y}={B}\right)\to {\phi }\right)$
8 7 2eximdv ${⊢}{\psi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {y}={B}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 6 8 syl5com ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$