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