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

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

Proof of Theorem imaeq2
StepHypRef Expression
1 reseq2 4966 . . 3  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
21rneqd 4922 . 2  |-  ( A  =  B  ->  ran  ( C  |`  A )  =  ran  ( C  |`  B ) )
3 df-ima 4718 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
4 df-ima 4718 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
52, 3, 43eqtr4g 2353 1  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   ran crn 4706    |` cres 4707   "cima 4708
This theorem is referenced by:  imaeq2i  5026  imaeq2d  5028  relimasn  5052  funimaexg  5345  ssimaex  5600  ssimaexg  5601  isoselem  5854  isowe2  5863  f1opw2  6087  fnse  6248  tz7.49  6473  ecexr  6681  fopwdom  6986  sbthlem2  6988  sbth  6997  ssenen  7051  domunfican  7145  fodomfi  7151  f1opwfi  7175  fipreima  7177  marypha1lem  7202  ordtypelem2  7250  ordtypelem3  7251  ordtypelem9  7257  dfac12lem2  7786  dfac12r  7788  ackbij2lem2  7882  ackbij2lem3  7883  r1om  7886  enfin2i  7963  zorn2lem6  8144  zorn2lem7  8145  isacs5lem  14288  acsdrscl  14289  gicsubgen  14758  efgrelexlema  15074  gsumval3  15207  tgcn  16998  subbascn  17000  cnpnei  17009  cnima  17010  iscncl  17014  cncls  17019  cnconst2  17027  cnrest2  17030  cnprest  17033  cnindis  17036  cncmp  17135  cmpfi  17151  2ndcomap  17200  ptbasfi  17292  xkoopn  17300  xkoccn  17329  txcnp  17330  ptcnplem  17331  txcnmpt  17334  ptrescn  17349  xkoco1cn  17367  xkoco2cn  17368  xkococn  17370  xkoinjcn  17397  elqtop  17404  qtopomap  17425  qtopcmap  17426  ordthmeolem  17508  fbasrn  17595  elfm  17658  elfm2  17659  elfm3  17661  imaelfm  17662  rnelfmlem  17663  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem3  17667  fmfnfmlem4  17668  fmco  17672  flffbas  17706  lmflf  17716  fcfneii  17748  ptcmplem3  17764  ptcmplem5  17766  ptcmpg  17767  symgtgp  17800  ghmcnp  17813  eltsms  17831  tsmsf1o  17843  metcnp3  18102  mbfdm  18999  ismbf  19001  mbfima  19003  ismbfd  19011  mbfimaopnlem  19026  mbfimaopn2  19028  i1fd  19052  ellimc2  19243  limcflf  19247  xrlimcnp  20279  ubthlem1  21465  disjpreima  23376  mbfmcnvima  23577  imambfm  23582  erdszelem1  23737  erdsze  23748  erdsze2lem2  23750  cvmscbv  23804  cvmsi  23811  cvmsval  23812  cvmliftlem15  23844  brimageg  24537  fnimage  24539  imageval  24540  fvimage  24541  oooeqim2  25156  intopcoaconlem3b  25641  intopcoaconlem3  25642  intopcoaconb  25643  iscnp4  25666  limptlimpr2lem2  25678  flfnei2  25680  smbkle  26146  cndpv  26152  pgapspf  26155  isibcg  26294  filnetlem4  26433  ismtyhmeolem  26631  ismtybndlem  26633  heibor1lem  26636  lmhmfgima  27285  csbfv12gALTVD  28991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-opab 4094  df-xp 4711  df-cnv 4713  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718
  Copyright terms: Public domain W3C validator