Theorem imaeq2 6013

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 5931	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5885	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5635	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5635	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2794	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

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

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635

This theorem is referenced by:  imaeq2i  6015  imaeq2d  6017  relimasn  6042  cnvimassrndm  6108  fimadmfo  6753  ssimaex  6917  ssimaexg  6918  isoselem  7285  isowe2  7294  f1opw2  7611  mptcnfimad  7928  fnse  8073  supp0cosupp0  8148  tz7.49  8374  ecexr  8638  fopwdom  9011  sbthlem2  9014  sbth  9023  ssenen  9077  sbthfi  9121  fodomfi  9210  imafiOLD  9214  domunfican  9220  fodomfiOLD  9228  f1opwfi  9254  fipreima  9256  marypha1lem  9334  ordtypelem2  9422  ordtypelem3  9423  ordtypelem9  9429  dfac12lem2  10053  dfac12r  10055  ackbij2lem2  10147  ackbij2lem3  10148  r1om  10151  enfin2i  10229  zorn2lem6  10409  zorn2lem7  10410  isacs5lem  18466  acsdrscl  18467  gicsubgen  19206  ghmqusnsglem1  19207  ghmquskerlem1  19210  ghmquskerco  19211  gicqusker  19215  efgrelexlema  19676  tgcn  23194  subbascn  23196  iscnp4  23205  cnpnei  23206  cnima  23207  iscncl  23211  cncls  23216  cnconst2  23225  cnrest2  23228  cnprest  23231  cnindis  23234  cncmp  23334  cmpfi  23350  2ndcomap  23400  ptbasfi  23523  xkoopn  23531  xkoccn  23561  txcnp  23562  ptcnplem  23563  txcnmpt  23566  ptrescn  23581  xkoco1cn  23599  xkoco2cn  23600  xkococn  23602  xkoinjcn  23629  elqtop  23639  qtopomap  23660  qtopcmap  23661  ordthmeolem  23743  fbasrn  23826  elfm  23889  elfm2  23890  elfm3  23892  imaelfm  23893  rnelfmlem  23894  rnelfm  23895  fmfnfmlem2  23897  fmfnfmlem3  23898  fmfnfmlem4  23899  fmco  23903  flffbas  23937  lmflf  23947  fcfneii  23979  ptcmplem3  23996  ptcmplem5  23998  ptcmpg  23999  cnextcn  24009  symgtgp  24048  ghmcnp  24057  eltsms  24075  tsmsf1o  24087  fmucnd  24233  ucnextcn  24245  metcnp3  24482  mbfdm  25581  ismbf  25583  mbfima  25585  ismbfd  25594  mbfimaopnlem  25610  mbfimaopn2  25612  i1fd  25636  ellimc2  25832  limcflf  25836  xrlimcnp  26932  oldval  27822  ubthlem1  30894  disjpreima  32608  imadifxp  32625  preimane  32697  fnpreimac  32698  lmicqusker  33448  ricqusker  33457  algextdeglem4  33826  algextdeg  33831  qtophaus  33942  rhmpreimacnlem  33990  rrhre  34127  mbfmcnvima  34361  imambfm  34368  eulerpartgbij  34478  erdszelem1  35334  erdsze  35345  erdsze2lem2  35347  cvmscbv  35401  cvmsi  35408  cvmsval  35409  cvmliftlem15  35441  opelco3  35918  brimageg  36068  fnimage  36070  imageval  36071  fvimage  36072  filnetlem4  36524  bj-imdirval3  37328  bj-imdirco  37334  ptrest  37759  ismtyhmeolem  37944  ismtybndlem  37946  heibor1lem  37949  zndvdchrrhm  42165  aks6d1c7lem2  42374  aks5lem4a  42383  lmhmfgima  43268  brtrclfv2  43910  csbfv12gALTVD  45081  icccncfext  46073  sge0f1o  46568  smfresal  46974  smfpimbor1lem1  46984  smfpimbor1lem2  46985  smfco  46988  f1cof1b  47265  fnfocofob  47267  imaelsetpreimafv  47583  fundcmpsurinjlem3  47588  imasetpreimafvbijlemfo  47593  fundcmpsurbijinjpreimafv  47595  grimco  48077  uhgrimedgi  48078  isuspgrim0  48082  isuspgrimlem  48083  upgrimwlklem5  48089  gricushgr  48105  grimedg  48123  grtrimap  48136  isubgr3stgrlem5  48158  isubgr3stgrlem6  48159  isubgr3stgrlem7  48160  isubgr3stgrlem8  48161  uspgrlimlem4  48179  grlimedgclnbgr  48183  grlimgrtrilem2  48190