Theorem imaeq2 6074

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
imaeq2	⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Proof of Theorem imaeq2

Step	Hyp	Ref	Expression
1		reseq2 5992	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5949	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5698	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5698	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2802	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  ran crn 5686   ↾ cres 5687   “ cima 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698

This theorem is referenced by:  imaeq2i  6076  imaeq2d  6078  relimasn  6103  cnvimassrndm  6172  funimaexgOLD  6654  fimadmfo  6829  ssimaex  6994  ssimaexg  6995  isoselem  7361  isowe2  7370  f1opw2  7688  mptcnfimad  8011  fnse  8158  supp0cosupp0  8233  tz7.49  8485  ecexr  8750  fopwdom  9120  sbthlem2  9124  sbth  9133  ssenen  9191  sbthfi  9239  fodomfi  9350  imafiOLD  9354  domunfican  9361  fodomfiOLD  9370  f1opwfi  9396  fipreima  9398  marypha1lem  9473  ordtypelem2  9559  ordtypelem3  9560  ordtypelem9  9566  dfac12lem2  10185  dfac12r  10187  ackbij2lem2  10279  ackbij2lem3  10280  r1om  10283  enfin2i  10361  zorn2lem6  10541  zorn2lem7  10542  isacs5lem  18590  acsdrscl  18591  gicsubgen  19297  ghmqusnsglem1  19298  ghmquskerlem1  19301  ghmquskerco  19302  gicqusker  19306  efgrelexlema  19767  tgcn  23260  subbascn  23262  iscnp4  23271  cnpnei  23272  cnima  23273  iscncl  23277  cncls  23282  cnconst2  23291  cnrest2  23294  cnprest  23297  cnindis  23300  cncmp  23400  cmpfi  23416  2ndcomap  23466  ptbasfi  23589  xkoopn  23597  xkoccn  23627  txcnp  23628  ptcnplem  23629  txcnmpt  23632  ptrescn  23647  xkoco1cn  23665  xkoco2cn  23666  xkococn  23668  xkoinjcn  23695  elqtop  23705  qtopomap  23726  qtopcmap  23727  ordthmeolem  23809  fbasrn  23892  elfm  23955  elfm2  23956  elfm3  23958  imaelfm  23959  rnelfmlem  23960  rnelfm  23961  fmfnfmlem2  23963  fmfnfmlem3  23964  fmfnfmlem4  23965  fmco  23969  flffbas  24003  lmflf  24013  fcfneii  24045  ptcmplem3  24062  ptcmplem5  24064  ptcmpg  24065  cnextcn  24075  symgtgp  24114  ghmcnp  24123  eltsms  24141  tsmsf1o  24153  fmucnd  24301  ucnextcn  24313  metcnp3  24553  mbfdm  25661  ismbf  25663  mbfima  25665  ismbfd  25674  mbfimaopnlem  25690  mbfimaopn2  25692  i1fd  25716  ellimc2  25912  limcflf  25916  xrlimcnp  27011  oldval  27893  ubthlem1  30889  disjpreima  32597  imadifxp  32614  preimane  32680  fnpreimac  32681  lmicqusker  33446  ricqusker  33455  algextdeglem4  33761  algextdeg  33766  qtophaus  33835  rhmpreimacnlem  33883  rrhre  34022  mbfmcnvima  34257  imambfm  34264  eulerpartgbij  34374  erdszelem1  35196  erdsze  35207  erdsze2lem2  35209  cvmscbv  35263  cvmsi  35270  cvmsval  35271  cvmliftlem15  35303  opelco3  35775  brimageg  35928  fnimage  35930  imageval  35931  fvimage  35932  filnetlem4  36382  bj-imdirval3  37185  bj-imdirco  37191  ptrest  37626  ismtyhmeolem  37811  ismtybndlem  37813  heibor1lem  37816  zndvdchrrhm  41972  aks6d1c7lem2  42182  aks5lem4a  42191  lmhmfgima  43096  brtrclfv2  43740  csbfv12gALTVD  44919  icccncfext  45902  sge0f1o  46397  smfresal  46803  smfpimbor1lem1  46813  smfpimbor1lem2  46814  smfco  46817  f1cof1b  47089  fnfocofob  47091  imaelsetpreimafv  47382  fundcmpsurinjlem3  47387  imasetpreimafvbijlemfo  47392  fundcmpsurbijinjpreimafv  47394  isuspgrim0  47872  uspgrimprop  47873  isuspgrimlem  47874  grimco  47880  gricushgr  47886  grimedg  47903  grtrimap  47915  isubgr3stgrlem5  47937  isubgr3stgrlem6  47938  isubgr3stgrlem7  47939  isubgr3stgrlem8  47940  uspgrlimlem4  47958  grlimgrtrilem2  47962