Theorem vtocl3

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011) Avoid ax-10 and ax-11 . (Revised by GG, 20-Aug-2023) (Proof shortened by Wolf Lammen, 23-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		vtocl3.1	$$⊢A\in \mathrm{V}$$
2		vtocl3.2	$$⊢B\in \mathrm{V}$$
3		vtocl3.3	$$⊢C\in \mathrm{V}$$
4		vtocl3.4	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
5		vtocl3.5	$$⊢\phi$$
6	5	a1i	$$⊢z=C\to \phi$$
7	4	3expa	$$⊢\left(\left(x=A\wedge y=B\right)\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
8	7	pm5.74da	$$⊢\left(x=A\wedge y=B\right)\to \left(\left(z=C\to \phi \right)\leftrightarrow \left(z=C\to \psi \right)\right)$$
9	1 2 8 6	vtocl2	$$⊢z=C\to \psi$$
10	6 9	2thd	$$⊢z=C\to \left(\phi \leftrightarrow \psi \right)$$
11	3 10 5	vtocl	$$⊢\psi$$