Theorem imaeq2 6064

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 5983	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5943	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5694	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5694	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2790	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1533  ran crn 5682   ↾ cres 5683   “ cima 5684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5687  df-cnv 5689  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694

This theorem is referenced by:  imaeq2i  6066  imaeq2d  6068  relimasn  6093  cnvimassrndm  6162  funimaexgOLD  6645  fimadmfo  6823  ssimaex  6986  ssimaexg  6987  isoselem  7352  isowe2  7361  f1opw2  7680  mptcnfimad  7999  fnse  8146  supp0cosupp0  8222  tz7.49  8474  ecexr  8738  fopwdom  9117  sbthlem2  9121  sbth  9130  ssenen  9188  imafi  9212  sbthfi  9239  domunfican  9358  fodomfi  9365  f1opwfi  9396  fipreima  9398  marypha1lem  9472  ordtypelem2  9558  ordtypelem3  9559  ordtypelem9  9565  dfac12lem2  10183  dfac12r  10185  ackbij2lem2  10279  ackbij2lem3  10280  r1om  10283  enfin2i  10360  zorn2lem6  10540  zorn2lem7  10541  isacs5lem  18565  acsdrscl  18566  gicsubgen  19268  ghmqusnsglem1  19269  ghmquskerlem1  19272  ghmquskerco  19273  gicqusker  19277  efgrelexlema  19742  tgcn  23239  subbascn  23241  iscnp4  23250  cnpnei  23251  cnima  23252  iscncl  23256  cncls  23261  cnconst2  23270  cnrest2  23273  cnprest  23276  cnindis  23279  cncmp  23379  cmpfi  23395  2ndcomap  23445  ptbasfi  23568  xkoopn  23576  xkoccn  23606  txcnp  23607  ptcnplem  23608  txcnmpt  23611  ptrescn  23626  xkoco1cn  23644  xkoco2cn  23645  xkococn  23647  xkoinjcn  23674  elqtop  23684  qtopomap  23705  qtopcmap  23706  ordthmeolem  23788  fbasrn  23871  elfm  23934  elfm2  23935  elfm3  23937  imaelfm  23938  rnelfmlem  23939  rnelfm  23940  fmfnfmlem2  23942  fmfnfmlem3  23943  fmfnfmlem4  23944  fmco  23948  flffbas  23982  lmflf  23992  fcfneii  24024  ptcmplem3  24041  ptcmplem5  24043  ptcmpg  24044  cnextcn  24054  symgtgp  24093  ghmcnp  24102  eltsms  24120  tsmsf1o  24132  fmucnd  24280  ucnextcn  24292  metcnp3  24532  mbfdm  25638  ismbf  25640  mbfima  25642  ismbfd  25651  mbfimaopnlem  25667  mbfimaopn2  25669  i1fd  25693  ellimc2  25889  limcflf  25893  xrlimcnp  26988  oldval  27870  ubthlem1  30795  disjpreima  32495  imadifxp  32512  preimane  32578  fnpreimac  32579  lmicqusker  33270  ricqusker  33279  algextdeglem4  33557  algextdeg  33562  qtophaus  33607  rhmpreimacnlem  33655  rrhre  33792  mbfmcnvima  34045  imambfm  34052  eulerpartgbij  34162  erdszelem1  34971  erdsze  34982  erdsze2lem2  34984  cvmscbv  35038  cvmsi  35045  cvmsval  35046  cvmliftlem15  35078  opelco3  35546  brimageg  35699  fnimage  35701  imageval  35702  fvimage  35703  filnetlem4  36041  bj-imdirval3  36839  bj-imdirco  36845  ptrest  37268  ismtyhmeolem  37453  ismtybndlem  37455  heibor1lem  37458  zndvdchrrhm  41617  aks6d1c7lem2  41827  lmhmfgima  42682  brtrclfv2  43331  csbfv12gALTVD  44512  icccncfext  45445  sge0f1o  45940  smfresal  46346  smfpimbor1lem1  46356  smfpimbor1lem2  46357  smfco  46360  f1cof1b  46627  fnfocofob  46629  imaelsetpreimafv  46904  fundcmpsurinjlem3  46909  imasetpreimafvbijlemfo  46914  fundcmpsurbijinjpreimafv  46916  isuspgrim0  47388  uspgrimprop  47389  isuspgrimlem  47390  grimco  47396  gricushgr  47402