Theorem vtocl2gf

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995)

	Ref	Expression
Hypotheses	vtocl2gf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	vtocl2gf.2	$$⊢\underset{\_}{Ⅎ}yA$$
	vtocl2gf.3	$$⊢\underset{\_}{Ⅎ}yB$$
	vtocl2gf.4	$$⊢Ⅎx\psi$$
	vtocl2gf.5	$$⊢Ⅎy\chi$$
	vtocl2gf.6	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	vtocl2gf.7	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
	vtocl2gf.8	$$⊢\phi$$
Assertion	vtocl2gf	$$⊢\left(A\in V\wedge B\in W\right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		vtocl2gf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		vtocl2gf.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		vtocl2gf.3	$$⊢\underset{\_}{Ⅎ}yB$$
4		vtocl2gf.4	$$⊢Ⅎx\psi$$
5		vtocl2gf.5	$$⊢Ⅎy\chi$$
6		vtocl2gf.6	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
7		vtocl2gf.7	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
8		vtocl2gf.8	$$⊢\phi$$
9		elex	$$⊢A\in V\to A\in \mathrm{V}$$
10	2	nfel1	$$⊢ℲyA\in \mathrm{V}$$
11	10 5	nfim	$$⊢Ⅎy\left(A\in \mathrm{V}\to \chi \right)$$
12	7	imbi2d	$$⊢y=B\to \left(\left(A\in \mathrm{V}\to \psi \right)\leftrightarrow \left(A\in \mathrm{V}\to \chi \right)\right)$$
13	1 4 6 8	vtoclgf	$$⊢A\in \mathrm{V}\to \psi$$
14	3 11 12 13	vtoclgf	$$⊢B\in W\to \left(A\in \mathrm{V}\to \chi \right)$$
15	9 14	mpan9	$$⊢\left(A\in V\wedge B\in W\right)\to \chi$$