vtocl2gaf

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

Step	Hyp	Ref	Expression
1		vtocl2gaf.a	$⊢ \underline{Ⅎ} x A$
2		vtocl2gaf.b	$⊢ \underline{Ⅎ} y A$
3		vtocl2gaf.c	$⊢ \underline{Ⅎ} y B$
4		vtocl2gaf.1	$⊢ Ⅎ x ψ$
5		vtocl2gaf.2	$⊢ Ⅎ y χ$
6		vtocl2gaf.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
7		vtocl2gaf.4	$⊢ y = B \to (ψ \leftrightarrow χ)$
8		vtocl2gaf.5	$⊢ (x \in C \land y \in D) \to φ$
9	1	nfel1	$⊢ Ⅎ x A \in C$
10		nfv	$⊢ Ⅎ x y \in D$
11	9 10	nfan	$⊢ Ⅎ x (A \in C \land y \in D)$
12	11 4	nfim	$⊢ Ⅎ x ((A \in C \land y \in D) \to ψ)$
13	2	nfel1	$⊢ Ⅎ y A \in C$
14	3	nfel1	$⊢ Ⅎ y B \in D$
15	13 14	nfan	$⊢ Ⅎ y (A \in C \land B \in D)$
16	15 5	nfim	$⊢ Ⅎ y ((A \in C \land B \in D) \to χ)$
17		eleq1	$⊢ x = A \to (x \in C \leftrightarrow A \in C)$
18	17	anbi1d	$⊢ x = A \to ((x \in C \land y \in D) \leftrightarrow (A \in C \land y \in D))$
19	18 6	imbi12d	$⊢ x = A \to (((x \in C \land y \in D) \to φ) \leftrightarrow ((A \in C \land y \in D) \to ψ))$
20		eleq1	$⊢ y = B \to (y \in D \leftrightarrow B \in D)$
21	20	anbi2d	$⊢ y = B \to ((A \in C \land y \in D) \leftrightarrow (A \in C \land B \in D))$
22	21 7	imbi12d	$⊢ y = B \to (((A \in C \land y \in D) \to ψ) \leftrightarrow ((A \in C \land B \in D) \to χ))$
23	1 2 3 12 16 19 22 8	vtocl2gf	$⊢ (A \in C \land B \in D) \to ((A \in C \land B \in D) \to χ)$
24	23	pm2.43i	$⊢ (A \in C \land B \in D) \to χ$

Metamath Proof Explorer