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

Theorem imaeq2 5008
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 4950 . . 3  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
21rneqd 4906 . 2  |-  ( A  =  B  ->  ran  ( C  |`  A )  =  ran  ( C  |`  B ) )
3 df-ima 4702 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
4 df-ima 4702 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
52, 3, 43eqtr4g 2340 1  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   ran crn 4690    |` cres 4691   "cima 4692
This theorem is referenced by:  imaeq2i  5010  imaeq2d  5012  relimasn  5036  funimaexg  5329  ssimaex  5584  ssimaexg  5585  isoselem  5838  isowe2  5847  f1opw2  6071  fnse  6232  tz7.49  6457  ecexr  6665  fopwdom  6970  sbthlem2  6972  sbth  6981  ssenen  7035  domunfican  7129  fodomfi  7135  f1opwfi  7159  fipreima  7161  marypha1lem  7186  ordtypelem2  7234  ordtypelem3  7235  ordtypelem9  7241  dfac12lem2  7770  dfac12r  7772  ackbij2lem2  7866  ackbij2lem3  7867  r1om  7870  enfin2i  7947  zorn2lem6  8128  zorn2lem7  8129  isacs5lem  14272  acsdrscl  14273  gicsubgen  14742  efgrelexlema  15058  gsumval3  15191  tgcn  16982  subbascn  16984  cnpnei  16993  cnima  16994  iscncl  16998  cncls  17003  cnconst2  17011  cnrest2  17014  cnprest  17017  cnindis  17020  cncmp  17119  cmpfi  17135  2ndcomap  17184  ptbasfi  17276  xkoopn  17284  xkoccn  17313  txcnp  17314  ptcnplem  17315  txcnmpt  17318  ptrescn  17333  xkoco1cn  17351  xkoco2cn  17352  xkococn  17354  xkoinjcn  17381  elqtop  17388  qtopomap  17409  qtopcmap  17410  ordthmeolem  17492  fbasrn  17579  elfm  17642  elfm2  17643  elfm3  17645  imaelfm  17646  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem3  17651  fmfnfmlem4  17652  fmco  17656  flffbas  17690  lmflf  17700  fcfneii  17732  ptcmplem3  17748  ptcmplem5  17750  ptcmpg  17751  symgtgp  17784  ghmcnp  17797  eltsms  17815  tsmsf1o  17827  metcnp3  18086  mbfdm  18983  ismbf  18985  mbfima  18987  ismbfd  18995  mbfimaopnlem  19010  mbfimaopn2  19012  i1fd  19036  ellimc2  19227  limcflf  19231  xrlimcnp  20263  ubthlem1  21449  disjpreima  23361  mbfmcnvima  23562  imambfm  23567  erdszelem1  23722  erdsze  23733  erdsze2lem2  23735  cvmscbv  23789  cvmsi  23796  cvmsval  23797  cvmliftlem15  23829  brimageg  24466  fnimage  24468  imageval  24469  fvimage  24470  funpartfun  24481  funpartfv  24483  oooeqim2  25053  intopcoaconlem3b  25538  intopcoaconlem3  25539  intopcoaconb  25540  iscnp4  25563  limptlimpr2lem2  25575  flfnei2  25577  smbkle  26043  cndpv  26049  pgapspf  26052  isibcg  26191  filnetlem4  26330  ismtyhmeolem  26528  ismtybndlem  26530  heibor1lem  26533  lmhmfgima  27182  csbfv12gALTVD  28675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702
  Copyright terms: Public domain W3C validator