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 ⊢ Ⅎ 𝑥 𝜑
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 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ) → 𝜒 )