Theorem vtocl2

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011)

	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	vtocl2	$$⊢\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	4	a1i	$$⊢y=B\to \phi$$
6	3	pm5.74da	$$⊢x=A\to \left(\left(y=B\to \phi \right)\leftrightarrow \left(y=B\to \psi \right)\right)$$
7	1 6 5	vtocl	$$⊢y=B\to \psi$$
8	5 7	2thd	$$⊢y=B\to \left(\phi \leftrightarrow \psi \right)$$
9	2 8 4	vtocl	$$⊢\psi$$