Metamath Proof Explorer


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 )