2gencl

Description: Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996)

	Ref	Expression
Hypotheses	2gencl.1	$⊢ C \in S \leftrightarrow \exists x \in R A = C$
	2gencl.2	$⊢ D \in S \leftrightarrow \exists y \in R B = D$
	2gencl.3	$⊢ A = C \to (φ \leftrightarrow ψ)$
	2gencl.4	$⊢ B = D \to (ψ \leftrightarrow χ)$
	2gencl.5	$⊢ (x \in R \land y \in R) \to φ$
Assertion	2gencl	$⊢ (C \in S \land D \in S) \to χ$

Step	Hyp	Ref	Expression
1		2gencl.1	$⊢ C \in S \leftrightarrow \exists x \in R A = C$
2		2gencl.2	$⊢ D \in S \leftrightarrow \exists y \in R B = D$
3		2gencl.3	$⊢ A = C \to (φ \leftrightarrow ψ)$
4		2gencl.4	$⊢ B = D \to (ψ \leftrightarrow χ)$
5		2gencl.5	$⊢ (x \in R \land y \in R) \to φ$
6		df-rex	$⊢ \exists y \in R B = D \leftrightarrow \exists y (y \in R \land B = D)$
7	2 6	bitri	$⊢ D \in S \leftrightarrow \exists y (y \in R \land B = D)$
8	4	imbi2d	$⊢ B = D \to ((C \in S \to ψ) \leftrightarrow (C \in S \to χ))$
9		df-rex	$⊢ \exists x \in R A = C \leftrightarrow \exists x (x \in R \land A = C)$
10	1 9	bitri	$⊢ C \in S \leftrightarrow \exists x (x \in R \land A = C)$
11	3	imbi2d	$⊢ A = C \to ((y \in R \to φ) \leftrightarrow (y \in R \to ψ))$
12	5	ex	$⊢ x \in R \to (y \in R \to φ)$
13	10 11 12	gencl	$⊢ C \in S \to (y \in R \to ψ)$
14	13	com12	$⊢ y \in R \to (C \in S \to ψ)$
15	7 8 14	gencl	$⊢ D \in S \to (C \in S \to χ)$
16	15	impcom	$⊢ (C \in S \land D \in S) \to χ$

Metamath Proof Explorer