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 ⊢ C ∈ S ↔ ∃ x ∈ R A = C
2gencl.2 ⊢ D ∈ S ↔ ∃ y ∈ R B = D
2gencl.3 ⊢ A = C → φ ↔ ψ
2gencl.4 ⊢ B = D → ψ ↔ χ
2gencl.5 ⊢ x ∈ R ∧ y ∈ R → φ
Assertion 2gencl ⊢ C ∈ S ∧ D ∈ S → χ

Proof

Step Hyp Ref Expression
1 2gencl.1 ⊢ C ∈ S ↔ ∃ x ∈ R A = C
2 2gencl.2 ⊢ D ∈ S ↔ ∃ y ∈ R B = D
3 2gencl.3 ⊢ A = C → φ ↔ ψ
4 2gencl.4 ⊢ B = D → ψ ↔ χ
5 2gencl.5 ⊢ x ∈ R ∧ y ∈ R → φ
6 df-rex ⊢ ∃ y ∈ R B = D ↔ ∃ y y ∈ R ∧ B = D
7 2 6 bitri ⊢ D ∈ S ↔ ∃ y y ∈ R ∧ B = D
8 4 imbi2d ⊢ B = D → C ∈ S → ψ ↔ C ∈ S → χ
9 df-rex ⊢ ∃ x ∈ R A = C ↔ ∃ x x ∈ R ∧ A = C
10 1 9 bitri ⊢ C ∈ S ↔ ∃ x x ∈ R ∧ A = C
11 3 imbi2d ⊢ A = C → y ∈ R → φ ↔ y ∈ R → ψ
12 5 ex ⊢ x ∈ R → y ∈ R → φ
13 10 11 12 gencl ⊢ C ∈ S → y ∈ R → ψ
14 13 com12 ⊢ y ∈ R → C ∈ S → ψ
15 7 8 14 gencl ⊢ D ∈ S → C ∈ S → χ
16 15 impcom ⊢ C ∈ S ∧ D ∈ S → χ