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

Metamath Proof Explorer

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 ⊢ ( ( 𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) → 𝜃 )