Theorem imaeq2 6016

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 5934	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5891	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5644	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5644	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  ran crn 5632   ↾ cres 5633   “ cima 5634

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  imaeq2i  6018  imaeq2d  6020  relimasn  6045  cnvimassrndm  6113  fimadmfo  6763  ssimaex  6928  ssimaexg  6929  isoselem  7298  isowe2  7307  f1opw2  7624  mptcnfimad  7944  fnse  8089  supp0cosupp0  8164  tz7.49  8390  ecexr  8653  fopwdom  9026  sbthlem2  9029  sbth  9038  ssenen  9092  sbthfi  9140  fodomfi  9237  imafiOLD  9241  domunfican  9248  fodomfiOLD  9257  f1opwfi  9283  fipreima  9285  marypha1lem  9360  ordtypelem2  9448  ordtypelem3  9449  ordtypelem9  9455  dfac12lem2  10074  dfac12r  10076  ackbij2lem2  10168  ackbij2lem3  10169  r1om  10172  enfin2i  10250  zorn2lem6  10430  zorn2lem7  10431  isacs5lem  18486  acsdrscl  18487  gicsubgen  19193  ghmqusnsglem1  19194  ghmquskerlem1  19197  ghmquskerco  19198  gicqusker  19202  efgrelexlema  19663  tgcn  23172  subbascn  23174  iscnp4  23183  cnpnei  23184  cnima  23185  iscncl  23189  cncls  23194  cnconst2  23203  cnrest2  23206  cnprest  23209  cnindis  23212  cncmp  23312  cmpfi  23328  2ndcomap  23378  ptbasfi  23501  xkoopn  23509  xkoccn  23539  txcnp  23540  ptcnplem  23541  txcnmpt  23544  ptrescn  23559  xkoco1cn  23577  xkoco2cn  23578  xkococn  23580  xkoinjcn  23607  elqtop  23617  qtopomap  23638  qtopcmap  23639  ordthmeolem  23721  fbasrn  23804  elfm  23867  elfm2  23868  elfm3  23870  imaelfm  23871  rnelfmlem  23872  rnelfm  23873  fmfnfmlem2  23875  fmfnfmlem3  23876  fmfnfmlem4  23877  fmco  23881  flffbas  23915  lmflf  23925  fcfneii  23957  ptcmplem3  23974  ptcmplem5  23976  ptcmpg  23977  cnextcn  23987  symgtgp  24026  ghmcnp  24035  eltsms  24053  tsmsf1o  24065  fmucnd  24212  ucnextcn  24224  metcnp3  24461  mbfdm  25560  ismbf  25562  mbfima  25564  ismbfd  25573  mbfimaopnlem  25589  mbfimaopn2  25591  i1fd  25615  ellimc2  25811  limcflf  25815  xrlimcnp  26911  oldval  27799  ubthlem1  30849  disjpreima  32563  imadifxp  32580  preimane  32644  fnpreimac  32645  lmicqusker  33382  ricqusker  33391  algextdeglem4  33703  algextdeg  33708  qtophaus  33819  rhmpreimacnlem  33867  rrhre  34004  mbfmcnvima  34239  imambfm  34246  eulerpartgbij  34356  erdszelem1  35171  erdsze  35182  erdsze2lem2  35184  cvmscbv  35238  cvmsi  35245  cvmsval  35246  cvmliftlem15  35278  opelco3  35755  brimageg  35908  fnimage  35910  imageval  35911  fvimage  35912  filnetlem4  36362  bj-imdirval3  37165  bj-imdirco  37171  ptrest  37606  ismtyhmeolem  37791  ismtybndlem  37793  heibor1lem  37796  zndvdchrrhm  41953  aks6d1c7lem2  42162  aks5lem4a  42171  lmhmfgima  43066  brtrclfv2  43709  csbfv12gALTVD  44881  icccncfext  45878  sge0f1o  46373  smfresal  46779  smfpimbor1lem1  46789  smfpimbor1lem2  46790  smfco  46793  f1cof1b  47071  fnfocofob  47073  imaelsetpreimafv  47389  fundcmpsurinjlem3  47394  imasetpreimafvbijlemfo  47399  fundcmpsurbijinjpreimafv  47401  grimco  47882  uhgrimedgi  47883  isuspgrim0  47887  isuspgrimlem  47888  upgrimwlklem5  47894  gricushgr  47910  grimedg  47928  grtrimap  47940  isubgr3stgrlem5  47962  isubgr3stgrlem6  47963  isubgr3stgrlem7  47964  isubgr3stgrlem8  47965  uspgrlimlem4  47983  grlimgrtrilem2  47987