Theorem vtocl2OLD

Description: Obsolete proof of vtocl2 as of 23-Aug-2023. (Contributed by NM, 26-Jul-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		vtocl2.1	$$⊢A\in \mathrm{V}$$
2		vtocl2.2	$$⊢B\in \mathrm{V}$$
3		vtocl2.3	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
4		vtocl2.4	$$⊢\phi$$
5	1	isseti	$$⊢\exists xx=A$$
6	2	isseti	$$⊢\exists yy=B$$
7		exdistrv	$$⊢\exists x\exists y\left(x=A\wedge y=B\right)\leftrightarrow \left(\exists xx=A\wedge \exists yy=B\right)$$
8	3	biimpd	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \to \psi \right)$$
9	8	2eximi	$$⊢\exists x\exists y\left(x=A\wedge y=B\right)\to \exists x\exists y\left(\phi \to \psi \right)$$
10	7 9	sylbir	$$⊢\left(\exists xx=A\wedge \exists yy=B\right)\to \exists x\exists y\left(\phi \to \psi \right)$$
11	5 6 10	mp2an	$$⊢\exists x\exists y\left(\phi \to \psi \right)$$
12		19.36v	$$⊢\exists y\left(\phi \to \psi \right)\leftrightarrow \left(\forall y\phi \to \psi \right)$$
13	12	exbii	$$⊢\exists x\exists y\left(\phi \to \psi \right)\leftrightarrow \exists x\left(\forall y\phi \to \psi \right)$$
14	11 13	mpbi	$$⊢\exists x\left(\forall y\phi \to \psi \right)$$
15	14	19.36iv	$$⊢\forall x\forall y\phi \to \psi$$
16	4	ax-gen	$$⊢\forall y\phi$$
17	15 16	mpg	$$⊢\psi$$