3gencl

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

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

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

Metamath Proof Explorer