This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → 𝜒 )