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	$$⊢\underset{\_}{Ⅎ}xA$$
	vtocl2gaf.b	$$⊢\underset{\_}{Ⅎ}yA$$
	vtocl2gaf.c	$$⊢\underset{\_}{Ⅎ}yB$$
	vtocl2gaf.1	$$⊢Ⅎx\psi$$
	vtocl2gaf.2	$$⊢Ⅎy\chi$$
	vtocl2gaf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	vtocl2gaf.4	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
	vtocl2gaf.5	$$⊢\left(x\in C\wedge y\in D\right)\to \phi$$
Assertion	vtocl2gaf	$$⊢\left(A\in C\wedge B\in D\right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		vtocl2gaf.a	$$⊢\underset{\_}{Ⅎ}xA$$
2		vtocl2gaf.b	$$⊢\underset{\_}{Ⅎ}yA$$
3		vtocl2gaf.c	$$⊢\underset{\_}{Ⅎ}yB$$
4		vtocl2gaf.1	$$⊢Ⅎx\psi$$
5		vtocl2gaf.2	$$⊢Ⅎy\chi$$
6		vtocl2gaf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
7		vtocl2gaf.4	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
8		vtocl2gaf.5	$$⊢\left(x\in C\wedge y\in D\right)\to \phi$$
9	2	nfel1	$$⊢ℲyA\in C$$
10	9 5	nfim	$$⊢Ⅎy\left(A\in C\to \chi \right)$$
11	7	imbi2d	$$⊢y=B\to \left(\left(A\in C\to \psi \right)\leftrightarrow \left(A\in C\to \chi \right)\right)$$
12		nfv	$$⊢Ⅎxy\in D$$
13	12 4	nfim	$$⊢Ⅎx\left(y\in D\to \psi \right)$$
14	6	imbi2d	$$⊢x=A\to \left(\left(y\in D\to \phi \right)\leftrightarrow \left(y\in D\to \psi \right)\right)$$
15	8	ex	$$⊢x\in C\to \left(y\in D\to \phi \right)$$
16	1 13 14 15	vtoclgaf	$$⊢A\in C\to \left(y\in D\to \psi \right)$$
17	16	com12	$$⊢y\in D\to \left(A\in C\to \psi \right)$$
18	3 10 11 17	vtoclgaf	$$⊢B\in D\to \left(A\in C\to \chi \right)$$
19	18	impcom	$$⊢\left(A\in C\wedge B\in D\right)\to \chi$$