This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \underline{Ⅎ} x A$
		vtocl2gaf.b	$⊢ \underline{Ⅎ} y A$
		vtocl2gaf.c	$⊢ \underline{Ⅎ} y B$
		vtocl2gaf.1	$⊢ Ⅎ x ψ$
		vtocl2gaf.2	$⊢ Ⅎ y χ$
		vtocl2gaf.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
		vtocl2gaf.4	$⊢ y = B \to (ψ \leftrightarrow χ)$
		vtocl2gaf.5	$⊢ (x \in C \land y \in D) \to φ$
	Assertion	vtocl2gaf	$⊢ (A \in C \land B \in D) \to χ$

Proof

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	2	nfel1	$⊢ Ⅎ y A \in C$
10	9 5	nfim	$⊢ Ⅎ y (A \in C \to χ)$
11	7	imbi2d	$⊢ y = B \to ((A \in C \to ψ) \leftrightarrow (A \in C \to χ))$
12		nfv	$⊢ Ⅎ x y \in D$
13	12 4	nfim	$⊢ Ⅎ x (y \in D \to ψ)$
14	6	imbi2d	$⊢ x = A \to ((y \in D \to φ) \leftrightarrow (y \in D \to ψ))$
15	8	ex	$⊢ x \in C \to (y \in D \to φ)$
16	1 13 14 15	vtoclgaf	$⊢ A \in C \to (y \in D \to ψ)$
17	16	com12	$⊢ y \in D \to (A \in C \to ψ)$
18	3 10 11 17	vtoclgaf	$⊢ B \in D \to (A \in C \to χ)$
19	18	impcom	$⊢ (A \in C \land B \in D) \to χ$