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

Metamath Proof Explorer

Theorem elabreximdv

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

Ref Expression
Hypotheses elabreximdv.1 ⊢ ( 𝐴 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
elabreximdv.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
elabreximdv.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝜓 )
Assertion elabreximdv ( ( 𝜑 ∧ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 elabreximdv.1 ⊢ ( 𝐴 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
2 elabreximdv.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 elabreximdv.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝜓 )
4 nfv ⊢ Ⅎ 𝑥 𝜑
5 nfv ⊢ Ⅎ 𝑥 𝜒
6 4 5 1 2 3 elabreximd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ) → 𝜒 )