Theorem elabreximdv

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

	Ref	Expression
Hypotheses	elabreximdv.1	|- ( A = B -> ( ch <-> ps ) )
	elabreximdv.2	|- ( ph -> A e. V )
	elabreximdv.3	|- ( ( ph /\ x e. C ) -> ps )
Assertion	elabreximdv	|- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		elabreximdv.1	|- ( A = B -> ( ch <-> ps ) )
2		elabreximdv.2	|- ( ph -> A e. V )
3		elabreximdv.3	|- ( ( ph /\ x e. C ) -> ps )
4		nfv	|- F/ x ph
5		nfv	|- F/ x ch
6	4 5 1 2 3	elabreximd	|- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> ch )