Metamath Proof Explorer

Theorem vtocl2ga

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023) (Proof shortened by Wolf Lammen, 23-Aug-2023)

		Ref	Expression
	Hypotheses	vtocl2ga.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
		vtocl2ga.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
		vtocl2ga.3	$⊢ (x \in C \land y \in D) \to φ$
	Assertion	vtocl2ga	$⊢ (A \in C \land B \in D) \to χ$

Proof

Step	Hyp	Ref	Expression
1		vtocl2ga.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		vtocl2ga.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		vtocl2ga.3	$⊢ (x \in C \land y \in D) \to φ$
4	2	imbi2d	$⊢ y = B \to ((A \in C \to ψ) \leftrightarrow (A \in C \to χ))$
5	1	imbi2d	$⊢ x = A \to ((y \in D \to φ) \leftrightarrow (y \in D \to ψ))$
6	3	ex	$⊢ x \in C \to (y \in D \to φ)$
7	5 6	vtoclga	$⊢ A \in C \to (y \in D \to ψ)$
8	7	com12	$⊢ y \in D \to (A \in C \to ψ)$
9	4 8	vtoclga	$⊢ B \in D \to (A \in C \to χ)$
10	9	impcom	$⊢ (A \in C \land B \in D) \to χ$