This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )