Theorem vtocl2gaf

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013)

	Ref	Expression
Hypotheses	vtocl2gaf.a	|- F/_ x A
	vtocl2gaf.b	|- F/_ y A
	vtocl2gaf.c	|- F/_ y B
	vtocl2gaf.1	|- F/ x ps
	vtocl2gaf.2	|- F/ y ch
	vtocl2gaf.3	|- ( x = A -> ( ph <-> ps ) )
	vtocl2gaf.4	|- ( y = B -> ( ps <-> ch ) )
	vtocl2gaf.5	|- ( ( x e. C /\ y e. D ) -> ph )
Assertion	vtocl2gaf	|- ( ( A e. C /\ B e. D ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		vtocl2gaf.a	|- F/_ x A
2		vtocl2gaf.b	|- F/_ y A
3		vtocl2gaf.c	|- F/_ y B
4		vtocl2gaf.1	|- F/ x ps
5		vtocl2gaf.2	|- F/ y ch
6		vtocl2gaf.3	|- ( x = A -> ( ph <-> ps ) )
7		vtocl2gaf.4	|- ( y = B -> ( ps <-> ch ) )
8		vtocl2gaf.5	|- ( ( x e. C /\ y e. D ) -> ph )
9	1	nfel1	|- F/ x A e. C
10		nfv	|- F/ x y e. D
11	9 10	nfan	|- F/ x ( A e. C /\ y e. D )
12	11 4	nfim	|- F/ x ( ( A e. C /\ y e. D ) -> ps )
13	2	nfel1	|- F/ y A e. C
14	3	nfel1	|- F/ y B e. D
15	13 14	nfan	|- F/ y ( A e. C /\ B e. D )
16	15 5	nfim	|- F/ y ( ( A e. C /\ B e. D ) -> ch )
17		eleq1	|- ( x = A -> ( x e. C <-> A e. C ) )
18	17	anbi1d	|- ( x = A -> ( ( x e. C /\ y e. D ) <-> ( A e. C /\ y e. D ) ) )
19	18 6	imbi12d	|- ( x = A -> ( ( ( x e. C /\ y e. D ) -> ph ) <-> ( ( A e. C /\ y e. D ) -> ps ) ) )
20		eleq1	|- ( y = B -> ( y e. D <-> B e. D ) )
21	20	anbi2d	|- ( y = B -> ( ( A e. C /\ y e. D ) <-> ( A e. C /\ B e. D ) ) )
22	21 7	imbi12d	|- ( y = B -> ( ( ( A e. C /\ y e. D ) -> ps ) <-> ( ( A e. C /\ B e. D ) -> ch ) ) )
23	1 2 3 12 16 19 22 8	vtocl2gf	|- ( ( A e. C /\ B e. D ) -> ( ( A e. C /\ B e. D ) -> ch ) )
24	23	pm2.43i	|- ( ( A e. C /\ B e. D ) -> ch )