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

Theorem imaeq2 5199
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 5141 . . 3  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
21rneqd 5097 . 2  |-  ( A  =  B  ->  ran  ( C  |`  A )  =  ran  ( C  |`  B ) )
3 df-ima 4891 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
4 df-ima 4891 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
52, 3, 43eqtr4g 2493 1  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   ran crn 4879    |` cres 4880   "cima 4881
This theorem is referenced by:  imaeq2i  5201  imaeq2d  5203  relimasn  5227  funimaexg  5530  ssimaex  5788  ssimaexg  5789  isoselem  6061  isowe2  6070  f1opw2  6298  fnse  6463  tz7.49  6702  ecexr  6910  fopwdom  7216  sbthlem2  7218  sbth  7227  ssenen  7281  domunfican  7379  fodomfi  7385  f1opwfi  7410  fipreima  7412  marypha1lem  7438  ordtypelem2  7488  ordtypelem3  7489  ordtypelem9  7495  dfac12lem2  8024  dfac12r  8026  ackbij2lem2  8120  ackbij2lem3  8121  r1om  8124  enfin2i  8201  zorn2lem6  8381  zorn2lem7  8382  isacs5lem  14595  acsdrscl  14596  gicsubgen  15065  efgrelexlema  15381  gsumval3  15514  tgcn  17316  subbascn  17318  iscnp4  17327  cnpnei  17328  cnima  17329  iscncl  17333  cncls  17338  cnconst2  17347  cnrest2  17350  cnprest  17353  cnindis  17356  cncmp  17455  cmpfi  17471  2ndcomap  17521  ptbasfi  17613  xkoopn  17621  xkoccn  17651  txcnp  17652  ptcnplem  17653  txcnmpt  17656  ptrescn  17671  xkoco1cn  17689  xkoco2cn  17690  xkococn  17692  xkoinjcn  17719  elqtop  17729  qtopomap  17750  qtopcmap  17751  ordthmeolem  17833  fbasrn  17916  elfm  17979  elfm2  17980  elfm3  17982  imaelfm  17983  rnelfmlem  17984  rnelfm  17985  fmfnfmlem2  17987  fmfnfmlem3  17988  fmfnfmlem4  17989  fmco  17993  flffbas  18027  lmflf  18037  fcfneii  18069  ptcmplem3  18085  ptcmplem5  18087  ptcmpg  18088  cnextcn  18098  symgtgp  18131  ghmcnp  18144  eltsms  18162  tsmsf1o  18174  fmucnd  18322  ucnextcn  18334  metcnp3  18570  mbfdm  19520  ismbf  19522  mbfima  19524  ismbfd  19532  mbfimaopnlem  19547  mbfimaopn2  19549  i1fd  19573  ellimc2  19764  limcflf  19768  xrlimcnp  20807  ubthlem1  22372  disjpreima  24026  imadifxp  24038  rrhre  24387  mbfmcnvima  24607  imambfm  24612  erdszelem1  24877  erdsze  24888  erdsze2lem2  24890  cvmscbv  24945  cvmsi  24952  cvmsval  24953  cvmliftlem15  24985  opelco3  25403  brimageg  25772  fnimage  25774  imageval  25775  fvimage  25776  filnetlem4  26410  ismtyhmeolem  26513  ismtybndlem  26515  heibor1lem  26518  lmhmfgima  27159  csbfv12gALTVD  29011
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-opab 4267  df-xp 4884  df-cnv 4886  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891
  Copyright terms: Public domain W3C validator