Theorem vtocl2gf

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

	Ref	Expression
Hypotheses	vtocl2gf.1	|- F/_ x A
	vtocl2gf.2	|- F/_ y A
	vtocl2gf.3	|- F/_ y B
	vtocl2gf.4	|- F/ x ps
	vtocl2gf.5	|- F/ y ch
	vtocl2gf.6	|- ( x = A -> ( ph <-> ps ) )
	vtocl2gf.7	|- ( y = B -> ( ps <-> ch ) )
	vtocl2gf.8	|- ph
Assertion	vtocl2gf	|- ( ( A e. V /\ B e. W ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		vtocl2gf.1	|- F/_ x A
2		vtocl2gf.2	|- F/_ y A
3		vtocl2gf.3	|- F/_ y B
4		vtocl2gf.4	|- F/ x ps
5		vtocl2gf.5	|- F/ y ch
6		vtocl2gf.6	|- ( x = A -> ( ph <-> ps ) )
7		vtocl2gf.7	|- ( y = B -> ( ps <-> ch ) )
8		vtocl2gf.8	|- ph
9		elex	|- ( A e. V -> A e. _V )
10	2	nfel1	|- F/ y A e. _V
11	10 5	nfim	|- F/ y ( A e. _V -> ch )
12	7	imbi2d	|- ( y = B -> ( ( A e. _V -> ps ) <-> ( A e. _V -> ch ) ) )
13	1 4 6 8	vtoclgf	|- ( A e. _V -> ps )
14	3 11 12 13	vtoclgf	|- ( B e. W -> ( A e. _V -> ch ) )
15	9 14	mpan9	|- ( ( A e. V /\ B e. W ) -> ch )