Theorem vtocl3gf

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013) (Revised by Mario Carneiro, 10-Oct-2016)

	Ref	Expression
Hypotheses	vtocl3gf.a	|- F/_ x A
	vtocl3gf.b	|- F/_ y A
	vtocl3gf.c	|- F/_ z A
	vtocl3gf.d	|- F/_ y B
	vtocl3gf.e	|- F/_ z B
	vtocl3gf.f	|- F/_ z C
	vtocl3gf.1	|- F/ x ps
	vtocl3gf.2	|- F/ y ch
	vtocl3gf.3	|- F/ z th
	vtocl3gf.4	|- ( x = A -> ( ph <-> ps ) )
	vtocl3gf.5	|- ( y = B -> ( ps <-> ch ) )
	vtocl3gf.6	|- ( z = C -> ( ch <-> th ) )
	vtocl3gf.7	|- ph
Assertion	vtocl3gf	|- ( ( A e. V /\ B e. W /\ C e. X ) -> th )

Proof

Step	Hyp	Ref	Expression
1		vtocl3gf.a	|- F/_ x A
2		vtocl3gf.b	|- F/_ y A
3		vtocl3gf.c	|- F/_ z A
4		vtocl3gf.d	|- F/_ y B
5		vtocl3gf.e	|- F/_ z B
6		vtocl3gf.f	|- F/_ z C
7		vtocl3gf.1	|- F/ x ps
8		vtocl3gf.2	|- F/ y ch
9		vtocl3gf.3	|- F/ z th
10		vtocl3gf.4	|- ( x = A -> ( ph <-> ps ) )
11		vtocl3gf.5	|- ( y = B -> ( ps <-> ch ) )
12		vtocl3gf.6	|- ( z = C -> ( ch <-> th ) )
13		vtocl3gf.7	|- ph
14		elex	|- ( A e. V -> A e. _V )
15	2	nfel1	|- F/ y A e. _V
16	15 8	nfim	|- F/ y ( A e. _V -> ch )
17	3	nfel1	|- F/ z A e. _V
18	17 9	nfim	|- F/ z ( A e. _V -> th )
19	11	imbi2d	|- ( y = B -> ( ( A e. _V -> ps ) <-> ( A e. _V -> ch ) ) )
20	12	imbi2d	|- ( z = C -> ( ( A e. _V -> ch ) <-> ( A e. _V -> th ) ) )
21	1 7 10 13	vtoclgf	|- ( A e. _V -> ps )
22	4 5 6 16 18 19 20 21	vtocl2gf	|- ( ( B e. W /\ C e. X ) -> ( A e. _V -> th ) )
23	14 22	mpan9	|- ( ( A e. V /\ ( B e. W /\ C e. X ) ) -> th )
24	23	3impb	|- ( ( A e. V /\ B e. W /\ C e. X ) -> th )