Theorem 3gencl

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

	Ref	Expression
Hypotheses	3gencl.1	⊢ ( 𝐷 ∈ 𝑆 ↔ ∃ 𝑥 ∈ 𝑅 𝐴 = 𝐷 )
	3gencl.2	⊢ ( 𝐹 ∈ 𝑆 ↔ ∃ 𝑦 ∈ 𝑅 𝐵 = 𝐹 )
	3gencl.3	⊢ ( 𝐺 ∈ 𝑆 ↔ ∃ 𝑧 ∈ 𝑅 𝐶 = 𝐺 )
	3gencl.4	⊢ ( 𝐴 = 𝐷 → ( 𝜑 ↔ 𝜓 ) )
	3gencl.5	⊢ ( 𝐵 = 𝐹 → ( 𝜓 ↔ 𝜒 ) )
	3gencl.6	⊢ ( 𝐶 = 𝐺 → ( 𝜒 ↔ 𝜃 ) )
	3gencl.7	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝜑 )
Assertion	3gencl	⊢ ( ( 𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		3gencl.1	⊢ ( 𝐷 ∈ 𝑆 ↔ ∃ 𝑥 ∈ 𝑅 𝐴 = 𝐷 )
2		3gencl.2	⊢ ( 𝐹 ∈ 𝑆 ↔ ∃ 𝑦 ∈ 𝑅 𝐵 = 𝐹 )
3		3gencl.3	⊢ ( 𝐺 ∈ 𝑆 ↔ ∃ 𝑧 ∈ 𝑅 𝐶 = 𝐺 )
4		3gencl.4	⊢ ( 𝐴 = 𝐷 → ( 𝜑 ↔ 𝜓 ) )
5		3gencl.5	⊢ ( 𝐵 = 𝐹 → ( 𝜓 ↔ 𝜒 ) )
6		3gencl.6	⊢ ( 𝐶 = 𝐺 → ( 𝜒 ↔ 𝜃 ) )
7		3gencl.7	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝜑 )
8		df-rex	⊢ ( ∃ 𝑧 ∈ 𝑅 𝐶 = 𝐺 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑅 ∧ 𝐶 = 𝐺 ) )
9	3 8	bitri	⊢ ( 𝐺 ∈ 𝑆 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑅 ∧ 𝐶 = 𝐺 ) )
10	6	imbi2d	⊢ ( 𝐶 = 𝐺 → ( ( ( 𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → 𝜒 ) ↔ ( ( 𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → 𝜃 ) ) )
11	4	imbi2d	⊢ ( 𝐴 = 𝐷 → ( ( 𝑧 ∈ 𝑅 → 𝜑 ) ↔ ( 𝑧 ∈ 𝑅 → 𝜓 ) ) )
12	5	imbi2d	⊢ ( 𝐵 = 𝐹 → ( ( 𝑧 ∈ 𝑅 → 𝜓 ) ↔ ( 𝑧 ∈ 𝑅 → 𝜒 ) ) )
13	7	3expia	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝑧 ∈ 𝑅 → 𝜑 ) )
14	1 2 11 12 13	2gencl	⊢ ( ( 𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝑧 ∈ 𝑅 → 𝜒 ) )
15	14	com12	⊢ ( 𝑧 ∈ 𝑅 → ( ( 𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → 𝜒 ) )
16	9 10 15	gencl	⊢ ( 𝐺 ∈ 𝑆 → ( ( 𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → 𝜃 ) )
17	16	com12	⊢ ( ( 𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐺 ∈ 𝑆 → 𝜃 ) )
18	17	3impia	⊢ ( ( 𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) → 𝜃 )