Theorem elabreximd

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

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

Proof

Step	Hyp	Ref	Expression
1		elabreximd.1	|- F/ x ph
2		elabreximd.2	|- F/ x ch
3		elabreximd.3	|- ( A = B -> ( ch <-> ps ) )
4		elabreximd.4	|- ( ph -> A e. V )
5		elabreximd.5	|- ( ( ph /\ x e. C ) -> ps )
6		eqeq1	|- ( y = A -> ( y = B <-> A = B ) )
7	6	rexbidv	|- ( y = A -> ( E. x e. C y = B <-> E. x e. C A = B ) )
8	7	elabg	|- ( A e. V -> ( A e. { y | E. x e. C y = B } <-> E. x e. C A = B ) )
9	4 8	syl	|- ( ph -> ( A e. { y | E. x e. C y = B } <-> E. x e. C A = B ) )
10	9	biimpa	|- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> E. x e. C A = B )
11		simpr	|- ( ( ( ph /\ x e. C ) /\ A = B ) -> A = B )
12	5	adantr	|- ( ( ( ph /\ x e. C ) /\ A = B ) -> ps )
13	3	biimpar	|- ( ( A = B /\ ps ) -> ch )
14	11 12 13	syl2anc	|- ( ( ( ph /\ x e. C ) /\ A = B ) -> ch )
15	14	exp31	|- ( ph -> ( x e. C -> ( A = B -> ch ) ) )
16	1 2 15	rexlimd	|- ( ph -> ( E. x e. C A = B -> ch ) )
17	16	imp	|- ( ( ph /\ E. x e. C A = B ) -> ch )
18	10 17	syldan	|- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> ch )