Theorem elabreximdv

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

	Ref	Expression
Hypotheses	elabreximdv.1	$$⊢A=B\to \left(\chi \leftrightarrow \psi \right)$$
	elabreximdv.2	$$⊢\phi \to A\in V$$
	elabreximdv.3	$$⊢\left(\phi \wedge x\in C\right)\to \psi$$
Assertion	elabreximdv	$$⊢\left(\phi \wedge A\in \left\{y|\exists x\in Cy=B\right\}\right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		elabreximdv.1	$$⊢A=B\to \left(\chi \leftrightarrow \psi \right)$$
2		elabreximdv.2	$$⊢\phi \to A\in V$$
3		elabreximdv.3	$$⊢\left(\phi \wedge x\in C\right)\to \psi$$
4		nfv	$$⊢Ⅎx\phi$$
5		nfv	$$⊢Ⅎx\chi$$
6	4 5 1 2 3	elabreximd	$$⊢\left(\phi \wedge A\in \left\{y|\exists x\in Cy=B\right\}\right)\to \chi$$