Theorem vtocl2gaf

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013) (Proof shortened by Wolf Lammen, 31-May-2025)

	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	2	nfel1	|- F/ y A e. C
10	9 5	nfim	|- F/ y ( A e. C -> ch )
11	7	imbi2d	|- ( y = B -> ( ( A e. C -> ps ) <-> ( A e. C -> ch ) ) )
12		nfv	|- F/ x y e. D
13	12 4	nfim	|- F/ x ( y e. D -> ps )
14	6	imbi2d	|- ( x = A -> ( ( y e. D -> ph ) <-> ( y e. D -> ps ) ) )
15	8	ex	|- ( x e. C -> ( y e. D -> ph ) )
16	1 13 14 15	vtoclgaf	|- ( A e. C -> ( y e. D -> ps ) )
17	16	com12	|- ( y e. D -> ( A e. C -> ps ) )
18	3 10 11 17	vtoclgaf	|- ( B e. D -> ( A e. C -> ch ) )
19	18	impcom	|- ( ( A e. C /\ B e. D ) -> ch )