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

Metamath Proof Explorer

Theorem elabreximd

Description: Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016)

Ref Expression
Hypotheses elabreximd.1 ⊢ Ⅎ x φ
elabreximd.2 ⊢ Ⅎ x χ
elabreximd.3 ⊢ A = B → χ ↔ ψ
elabreximd.4 ⊢ φ → A ∈ V
elabreximd.5 ⊢ φ ∧ x ∈ C → ψ
Assertion elabreximd ⊢ φ ∧ A ∈ y | ∃ x ∈ C y = B → χ

Proof

Step Hyp Ref Expression
1 elabreximd.1 ⊢ Ⅎ x φ
2 elabreximd.2 ⊢ Ⅎ x χ
3 elabreximd.3 ⊢ A = B → χ ↔ ψ
4 elabreximd.4 ⊢ φ → A ∈ V
5 elabreximd.5 ⊢ φ ∧ x ∈ C → ψ
6 eqeq1 ⊢ y = A → y = B ↔ A = B
7 6 rexbidv ⊢ y = A → ∃ x ∈ C y = B ↔ ∃ x ∈ C A = B
8 7 elabg ⊢ A ∈ V → A ∈ y | ∃ x ∈ C y = B ↔ ∃ x ∈ C A = B
9 4 8 syl ⊢ φ → A ∈ y | ∃ x ∈ C y = B ↔ ∃ x ∈ C A = B
10 9 biimpa ⊢ φ ∧ A ∈ y | ∃ x ∈ C y = B → ∃ x ∈ C A = B
11 simpr ⊢ φ ∧ x ∈ C ∧ A = B → A = B
12 5 adantr ⊢ φ ∧ x ∈ C ∧ A = B → ψ
13 3 biimpar ⊢ A = B ∧ ψ → χ
14 11 12 13 syl2anc ⊢ φ ∧ x ∈ C ∧ A = B → χ
15 14 exp31 ⊢ φ → x ∈ C → A = B → χ
16 1 2 15 rexlimd ⊢ φ → ∃ x ∈ C A = B → χ
17 16 imp ⊢ φ ∧ ∃ x ∈ C A = B → χ
18 10 17 syldan ⊢ φ ∧ A ∈ y | ∃ x ∈ C y = B → χ