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

Theorem imaeq2 5898
Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
imaeq2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem imaeq2
StepHypRef Expression
1 reseq2 5821 . . 3 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
21rneqd 5781 . 2 (𝐴 = 𝐵 → ran (𝐶𝐴) = ran (𝐶𝐵))
3 df-ima 5541 . 2 (𝐶𝐴) = ran (𝐶𝐴)
4 df-ima 5541 . 2 (𝐶𝐵) = ran (𝐶𝐵)
52, 3, 43eqtr4g 2881 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  ran crn 5529  cres 5530  cima 5531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-br 5040  df-opab 5102  df-xp 5534  df-cnv 5536  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541
This theorem is referenced by:  imaeq2i  5900  imaeq2d  5902  relimasn  5925  funimaexg  6413  fimadmfo  6572  ssimaex  6721  ssimaexg  6722  isoselem  7068  isowe2  7077  f1opw2  7375  fnse  7802  supp0cosupp0  7847  supp0cosupp0OLD  7848  tz7.49  8056  ecexr  8269  fopwdom  8600  sbthlem2  8604  sbth  8613  ssenen  8667  domunfican  8767  fodomfi  8773  f1opwfi  8804  fipreima  8806  marypha1lem  8873  ordtypelem2  8959  ordtypelem3  8960  ordtypelem9  8966  dfac12lem2  9547  dfac12r  9549  ackbij2lem2  9639  ackbij2lem3  9640  r1om  9643  enfin2i  9720  zorn2lem6  9900  zorn2lem7  9901  isacs5lem  17758  acsdrscl  17759  gicsubgen  18397  efgrelexlema  18854  tgcn  21836  subbascn  21838  iscnp4  21847  cnpnei  21848  cnima  21849  iscncl  21853  cncls  21858  cnconst2  21867  cnrest2  21870  cnprest  21873  cnindis  21876  cncmp  21976  cmpfi  21992  2ndcomap  22042  ptbasfi  22165  xkoopn  22173  xkoccn  22203  txcnp  22204  ptcnplem  22205  txcnmpt  22208  ptrescn  22223  xkoco1cn  22241  xkoco2cn  22242  xkococn  22244  xkoinjcn  22271  elqtop  22281  qtopomap  22302  qtopcmap  22303  ordthmeolem  22385  fbasrn  22468  elfm  22531  elfm2  22532  elfm3  22534  imaelfm  22535  rnelfmlem  22536  rnelfm  22537  fmfnfmlem2  22539  fmfnfmlem3  22540  fmfnfmlem4  22541  fmco  22545  flffbas  22579  lmflf  22589  fcfneii  22621  ptcmplem3  22638  ptcmplem5  22640  ptcmpg  22641  cnextcn  22651  symgtgp  22690  ghmcnp  22699  eltsms  22717  tsmsf1o  22729  fmucnd  22877  ucnextcn  22889  metcnp3  23126  mbfdm  24209  ismbf  24211  mbfima  24213  ismbfd  24222  mbfimaopnlem  24238  mbfimaopn2  24240  i1fd  24264  ellimc2  24459  limcflf  24463  xrlimcnp  25533  ubthlem1  28632  disjpreima  30321  imadifxp  30338  preimane  30402  fnpreimac  30403  qtophaus  31111  rrhre  31270  mbfmcnvima  31523  imambfm  31528  eulerpartgbij  31638  erdszelem1  32446  erdsze  32457  erdsze2lem2  32459  cvmscbv  32513  cvmsi  32520  cvmsval  32521  cvmliftlem15  32553  opelco3  33026  brimageg  33396  fnimage  33398  imageval  33399  fvimage  33400  filnetlem4  33737  bj-imdirval3  34492  bj-imdirco  34497  ptrest  34942  ismtyhmeolem  35128  ismtybndlem  35130  heibor1lem  35133  lmhmfgima  39839  brtrclfv2  40239  csbfv12gALTVD  41420  icccncfext  42352  sge0f1o  42844  smfresal  43243  smfpimbor1lem1  43253  smfpimbor1lem2  43254  smfco  43257  imaelsetpreimafv  43735  fundcmpsurinjlem3  43740  imasetpreimafvbijlemfo  43745  fundcmpsurbijinjpreimafv  43747  isomushgr  44167  isomuspgrlem1  44168  isomuspgrlem2a  44169  isomuspgrlem2b  44170  isomuspgrlem2c  44171  isomuspgrlem2d  44172  isomuspgr  44175  isomgrsym  44177
  Copyright terms: Public domain W3C validator