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

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

Proof of Theorem imaeq2
StepHypRef Expression
1 reseq2 5842 . . 3 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
21rneqd 5802 . 2 (𝐴 = 𝐵 → ran (𝐶𝐴) = ran (𝐶𝐵))
3 df-ima 5562 . 2 (𝐶𝐴) = ran (𝐶𝐴)
4 df-ima 5562 . 2 (𝐶𝐵) = ran (𝐶𝐵)
52, 3, 43eqtr4g 2881 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  ran crn 5550  cres 5551  cima 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-xp 5555  df-cnv 5557  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562
This theorem is referenced by:  imaeq2i  5921  imaeq2d  5923  relimasn  5946  funimaexg  6434  fimadmfo  6593  ssimaex  6742  ssimaexg  6743  isoselem  7083  isowe2  7092  f1opw2  7389  fnse  7818  supp0cosupp0  7863  supp0cosupp0OLD  7864  tz7.49  8072  ecexr  8284  fopwdom  8614  sbthlem2  8617  sbth  8626  ssenen  8680  domunfican  8780  fodomfi  8786  f1opwfi  8817  fipreima  8819  marypha1lem  8886  ordtypelem2  8972  ordtypelem3  8973  ordtypelem9  8979  dfac12lem2  9559  dfac12r  9561  ackbij2lem2  9651  ackbij2lem3  9652  r1om  9655  enfin2i  9732  zorn2lem6  9912  zorn2lem7  9913  isacs5lem  17769  acsdrscl  17770  gicsubgen  18358  efgrelexlema  18806  tgcn  21790  subbascn  21792  iscnp4  21801  cnpnei  21802  cnima  21803  iscncl  21807  cncls  21812  cnconst2  21821  cnrest2  21824  cnprest  21827  cnindis  21830  cncmp  21930  cmpfi  21946  2ndcomap  21996  ptbasfi  22119  xkoopn  22127  xkoccn  22157  txcnp  22158  ptcnplem  22159  txcnmpt  22162  ptrescn  22177  xkoco1cn  22195  xkoco2cn  22196  xkococn  22198  xkoinjcn  22225  elqtop  22235  qtopomap  22256  qtopcmap  22257  ordthmeolem  22339  fbasrn  22422  elfm  22485  elfm2  22486  elfm3  22488  imaelfm  22489  rnelfmlem  22490  rnelfm  22491  fmfnfmlem2  22493  fmfnfmlem3  22494  fmfnfmlem4  22495  fmco  22499  flffbas  22533  lmflf  22543  fcfneii  22575  ptcmplem3  22592  ptcmplem5  22594  ptcmpg  22595  cnextcn  22605  symgtgp  22639  ghmcnp  22652  eltsms  22670  tsmsf1o  22682  fmucnd  22830  ucnextcn  22842  metcnp3  23079  mbfdm  24156  ismbf  24158  mbfima  24160  ismbfd  24169  mbfimaopnlem  24185  mbfimaopn2  24187  i1fd  24211  ellimc2  24404  limcflf  24408  xrlimcnp  25474  ubthlem1  28575  disjpreima  30263  imadifxp  30280  preimane  30344  fnpreimac  30345  qtophaus  31000  rrhre  31162  mbfmcnvima  31415  imambfm  31420  eulerpartgbij  31530  erdszelem1  32336  erdsze  32347  erdsze2lem2  32349  cvmscbv  32403  cvmsi  32410  cvmsval  32411  cvmliftlem15  32443  opelco3  32916  brimageg  33286  fnimage  33288  imageval  33289  fvimage  33290  filnetlem4  33627  bj-imdirval3  34367  ptrest  34773  ismtyhmeolem  34965  ismtybndlem  34967  heibor1lem  34970  lmhmfgima  39564  brtrclfv2  39952  csbfv12gALTVD  41113  icccncfext  42050  sge0f1o  42545  smfresal  42944  smfpimbor1lem1  42954  smfpimbor1lem2  42955  smfco  42958  isomushgr  43838  isomuspgrlem1  43839  isomuspgrlem2a  43840  isomuspgrlem2b  43841  isomuspgrlem2c  43842  isomuspgrlem2d  43843  isomuspgr  43846  isomgrsym  43848
  Copyright terms: Public domain W3C validator