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