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 \leftrightarrow \psi \right)$$
Assertion	spc2egv	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\psi \to \exists x\exists y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spc2egv.1	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		elisset	$$⊢A\in V\to \exists xx=A$$
3		elisset	$$⊢B\in W\to \exists yy=B$$
4	2 3	anim12i	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\exists xx=A\wedge \exists yy=B\right)$$
5		exdistrv	$$⊢\exists x\exists y\left(x=A\wedge y=B\right)\leftrightarrow \left(\exists xx=A\wedge \exists yy=B\right)$$
6	4 5	sylibr	$$⊢\left(A\in V\wedge B\in W\right)\to \exists x\exists y\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\exists y\left(x=A\wedge y=B\right)\to \exists x\exists y\phi \right)$$
9	6 8	syl5com	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\psi \to \exists x\exists y\phi \right)$$