MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imaeq1 Structured version   Visualization version   Unicode version

Theorem imaeq1 5169
Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
imaeq1  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )

Proof of Theorem imaeq1
StepHypRef Expression
1 reseq1 5105 . . 3  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
21rneqd 5068 . 2  |-  ( A  =  B  ->  ran  ( A  |`  C )  =  ran  ( B  |`  C ) )
3 df-ima 4852 . 2  |-  ( A
" C )  =  ran  ( A  |`  C )
4 df-ima 4852 . 2  |-  ( B
" C )  =  ran  ( B  |`  C )
52, 3, 43eqtr4g 2530 1  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452   ran crn 4840    |` cres 4841   "cima 4842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-cnv 4847  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852
This theorem is referenced by:  imaeq1i  5171  imaeq1d  5173  suppval  6935  eceq2  7419  marypha1lem  7965  marypha1  7966  ackbij2lem2  8688  ackbij2lem3  8689  r1om  8692  limsupval  13608  limsupvalOLD  13609  isacs1i  15641  mreacs  15642  islindf  19447  iscnp  20330  xkoccn  20711  xkohaus  20745  xkoco1cn  20749  xkoco2cn  20750  xkococnlem  20751  xkococn  20752  xkoinjcn  20779  fmval  21036  fmf  21038  utoptop  21327  restutop  21330  restutopopn  21331  ustuqtoplem  21332  ustuqtop1  21334  ustuqtop2  21335  ustuqtop4  21337  ustuqtop5  21338  utopsnneiplem  21340  utopsnnei  21342  neipcfilu  21389  psmetutop  21660  cfilfval  22312  elply2  23229  coeeu  23258  coelem  23259  coeeq  23260  dmarea  23962  mclsax  30279  tailfval  31099  bj-cleq  31625  poimirlem15  32019  poimirlem24  32028  brtrclfv2  36390
  Copyright terms: Public domain W3C validator