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

Theorem imaeq1 5163
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 5099 . . 3  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
21rneqd 5062 . 2  |-  ( A  =  B  ->  ran  ( A  |`  C )  =  ran  ( B  |`  C ) )
3 df-ima 4847 . 2  |-  ( A
" C )  =  ran  ( A  |`  C )
4 df-ima 4847 . 2  |-  ( B
" C )  =  ran  ( B  |`  C )
52, 3, 43eqtr4g 2510 1  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444   ran crn 4835    |` cres 4836   "cima 4837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403  df-opab 4462  df-cnv 4842  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847
This theorem is referenced by:  imaeq1i  5165  imaeq1d  5167  suppval  6916  eceq2  7401  marypha1lem  7947  marypha1  7948  ackbij2lem2  8670  ackbij2lem3  8671  r1om  8674  limsupval  13531  limsupvalOLD  13532  isacs1i  15563  mreacs  15564  islindf  19370  iscnp  20253  xkoccn  20634  xkohaus  20668  xkoco1cn  20672  xkoco2cn  20673  xkococnlem  20674  xkococn  20675  xkoinjcn  20702  fmval  20958  fmf  20960  utoptop  21249  restutop  21252  restutopopn  21253  ustuqtoplem  21254  ustuqtop1  21256  ustuqtop2  21257  ustuqtop4  21259  ustuqtop5  21260  utopsnneiplem  21262  utopsnnei  21264  neipcfilu  21311  psmetutop  21582  cfilfval  22234  elply2  23150  coeeu  23179  coelem  23180  coeeq  23181  dmarea  23883  mclsax  30207  tailfval  31028  bj-cleq  31555  poimirlem15  31955  poimirlem24  31964  brtrclfv2  36319
  Copyright terms: Public domain W3C validator