Theorem 2gencl

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

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

Proof

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