Theorem spc2ev

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

	Ref	Expression
Hypotheses	spc2ev.1	$$⊢A\in \mathrm{V}$$
	spc2ev.2	$$⊢B\in \mathrm{V}$$
	spc2ev.3	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	spc2ev	$$⊢\psi \to \exists x\exists y\phi$$

Proof

Step	Hyp	Ref	Expression
1		spc2ev.1	$$⊢A\in \mathrm{V}$$
2		spc2ev.2	$$⊢B\in \mathrm{V}$$
3		spc2ev.3	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
4	3	spc2egv	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(\psi \to \exists x\exists y\phi \right)$$
5	1 2 4	mp2an	$$⊢\psi \to \exists x\exists y\phi$$