Theorem imaeq2 6015

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 5933	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5887	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5637	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5637	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1541  ran crn 5625   ↾ cres 5626   “ cima 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  imaeq2i  6017  imaeq2d  6019  relimasn  6044  cnvimassrndm  6110  fimadmfo  6755  ssimaex  6919  ssimaexg  6920  isoselem  7287  isowe2  7296  f1opw2  7613  mptcnfimad  7930  fnse  8075  supp0cosupp0  8150  tz7.49  8376  ecexr  8640  fopwdom  9013  sbthlem2  9016  sbth  9025  ssenen  9079  sbthfi  9123  fodomfi  9212  imafiOLD  9216  domunfican  9222  fodomfiOLD  9230  f1opwfi  9256  fipreima  9258  marypha1lem  9336  ordtypelem2  9424  ordtypelem3  9425  ordtypelem9  9431  dfac12lem2  10055  dfac12r  10057  ackbij2lem2  10149  ackbij2lem3  10150  r1om  10153  enfin2i  10231  zorn2lem6  10411  zorn2lem7  10412  isacs5lem  18468  acsdrscl  18469  gicsubgen  19208  ghmqusnsglem1  19209  ghmquskerlem1  19212  ghmquskerco  19213  gicqusker  19217  efgrelexlema  19678  tgcn  23196  subbascn  23198  iscnp4  23207  cnpnei  23208  cnima  23209  iscncl  23213  cncls  23218  cnconst2  23227  cnrest2  23230  cnprest  23233  cnindis  23236  cncmp  23336  cmpfi  23352  2ndcomap  23402  ptbasfi  23525  xkoopn  23533  xkoccn  23563  txcnp  23564  ptcnplem  23565  txcnmpt  23568  ptrescn  23583  xkoco1cn  23601  xkoco2cn  23602  xkococn  23604  xkoinjcn  23631  elqtop  23641  qtopomap  23662  qtopcmap  23663  ordthmeolem  23745  fbasrn  23828  elfm  23891  elfm2  23892  elfm3  23894  imaelfm  23895  rnelfmlem  23896  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem3  23900  fmfnfmlem4  23901  fmco  23905  flffbas  23939  lmflf  23949  fcfneii  23981  ptcmplem3  23998  ptcmplem5  24000  ptcmpg  24001  cnextcn  24011  symgtgp  24050  ghmcnp  24059  eltsms  24077  tsmsf1o  24089  fmucnd  24235  ucnextcn  24247  metcnp3  24484  mbfdm  25583  ismbf  25585  mbfima  25587  ismbfd  25596  mbfimaopnlem  25612  mbfimaopn2  25614  i1fd  25638  ellimc2  25834  limcflf  25838  xrlimcnp  26934  oldval  27830  ubthlem1  30945  disjpreima  32659  imadifxp  32676  preimane  32748  fnpreimac  32749  lmicqusker  33499  ricqusker  33508  algextdeglem4  33877  algextdeg  33882  qtophaus  33993  rhmpreimacnlem  34041  rrhre  34178  mbfmcnvima  34412  imambfm  34419  eulerpartgbij  34529  erdszelem1  35385  erdsze  35396  erdsze2lem2  35398  cvmscbv  35452  cvmsi  35459  cvmsval  35460  cvmliftlem15  35492  opelco3  35969  brimageg  36119  fnimage  36121  imageval  36122  fvimage  36123  filnetlem4  36575  bj-imdirval3  37389  bj-imdirco  37395  ptrest  37820  ismtyhmeolem  38005  ismtybndlem  38007  heibor1lem  38010  zndvdchrrhm  42226  aks6d1c7lem2  42435  aks5lem4a  42444  lmhmfgima  43326  brtrclfv2  43968  csbfv12gALTVD  45139  icccncfext  46131  sge0f1o  46626  smfresal  47032  smfpimbor1lem1  47042  smfpimbor1lem2  47043  smfco  47046  f1cof1b  47323  fnfocofob  47325  imaelsetpreimafv  47641  fundcmpsurinjlem3  47646  imasetpreimafvbijlemfo  47651  fundcmpsurbijinjpreimafv  47653  grimco  48135  uhgrimedgi  48136  isuspgrim0  48140  isuspgrimlem  48141  upgrimwlklem5  48147  gricushgr  48163  grimedg  48181  grtrimap  48194  isubgr3stgrlem5  48216  isubgr3stgrlem6  48217  isubgr3stgrlem7  48218  isubgr3stgrlem8  48219  uspgrlimlem4  48237  grlimedgclnbgr  48241  grlimgrtrilem2  48248