Theorem vtocl2g

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995) Remove dependency on ax-10 , ax-11 , and ax-13 . (Revised by Steven Nguyen, 29-Nov-2022)

	Ref	Expression
Hypotheses	vtocl2g.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	vtocl2g.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
	vtocl2g.3	$$⊢\phi$$
Assertion	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		vtocl2g.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		vtocl2g.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
3		vtocl2g.3	$$⊢\phi$$
4		elex	$$⊢A\in V\to A\in \mathrm{V}$$
5	2	imbi2d	$$⊢y=B\to \left(\left(A\in \mathrm{V}\to \psi \right)\leftrightarrow \left(A\in \mathrm{V}\to \chi \right)\right)$$
6	1 3	vtoclg	$$⊢A\in \mathrm{V}\to \psi$$
7	5 6	vtoclg	$$⊢B\in W\to \left(A\in \mathrm{V}\to \chi \right)$$
8	4 7	mpan9	$$⊢\left(A\in V\wedge B\in W\right)\to \chi$$