# Metamath Proof Explorer

## Theorem elabreximd

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

Ref Expression
Hypotheses elabreximd.1 𝑥 𝜑
elabreximd.2 𝑥 𝜒
elabreximd.3 ( 𝐴 = 𝐵 → ( 𝜒𝜓 ) )
elabreximd.4 ( 𝜑𝐴𝑉 )
elabreximd.5 ( ( 𝜑𝑥𝐶 ) → 𝜓 )
Assertion elabreximd ( ( 𝜑𝐴 ∈ { 𝑦 ∣ ∃ 𝑥𝐶 𝑦 = 𝐵 } ) → 𝜒 )

### Proof

Step Hyp Ref Expression
1 elabreximd.1 𝑥 𝜑
2 elabreximd.2 𝑥 𝜒
3 elabreximd.3 ( 𝐴 = 𝐵 → ( 𝜒𝜓 ) )
4 elabreximd.4 ( 𝜑𝐴𝑉 )
5 elabreximd.5 ( ( 𝜑𝑥𝐶 ) → 𝜓 )
6 eqeq1 ( 𝑦 = 𝐴 → ( 𝑦 = 𝐵𝐴 = 𝐵 ) )
7 6 rexbidv ( 𝑦 = 𝐴 → ( ∃ 𝑥𝐶 𝑦 = 𝐵 ↔ ∃ 𝑥𝐶 𝐴 = 𝐵 ) )
8 7 elabg ( 𝐴𝑉 → ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥𝐶 𝑦 = 𝐵 } ↔ ∃ 𝑥𝐶 𝐴 = 𝐵 ) )
9 4 8 syl ( 𝜑 → ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥𝐶 𝑦 = 𝐵 } ↔ ∃ 𝑥𝐶 𝐴 = 𝐵 ) )
10 9 biimpa ( ( 𝜑𝐴 ∈ { 𝑦 ∣ ∃ 𝑥𝐶 𝑦 = 𝐵 } ) → ∃ 𝑥𝐶 𝐴 = 𝐵 )
11 simpr ( ( ( 𝜑𝑥𝐶 ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
12 5 adantr ( ( ( 𝜑𝑥𝐶 ) ∧ 𝐴 = 𝐵 ) → 𝜓 )
13 3 biimpar ( ( 𝐴 = 𝐵𝜓 ) → 𝜒 )
14 11 12 13 syl2anc ( ( ( 𝜑𝑥𝐶 ) ∧ 𝐴 = 𝐵 ) → 𝜒 )
15 14 exp31 ( 𝜑 → ( 𝑥𝐶 → ( 𝐴 = 𝐵𝜒 ) ) )
16 1 2 15 rexlimd ( 𝜑 → ( ∃ 𝑥𝐶 𝐴 = 𝐵𝜒 ) )
17 16 imp ( ( 𝜑 ∧ ∃ 𝑥𝐶 𝐴 = 𝐵 ) → 𝜒 )
18 10 17 syldan ( ( 𝜑𝐴 ∈ { 𝑦 ∣ ∃ 𝑥𝐶 𝑦 = 𝐵 } ) → 𝜒 )
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}