Theorem imaeq2 6075

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 5994	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5951	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5701	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5701	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1536  ran crn 5689   ↾ cres 5690   “ cima 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701

This theorem is referenced by:  imaeq2i  6077  imaeq2d  6079  relimasn  6104  cnvimassrndm  6173  funimaexgOLD  6654  fimadmfo  6829  ssimaex  6993  ssimaexg  6994  isoselem  7360  isowe2  7369  f1opw2  7687  mptcnfimad  8009  fnse  8156  supp0cosupp0  8231  tz7.49  8483  ecexr  8748  fopwdom  9118  sbthlem2  9122  sbth  9131  ssenen  9189  sbthfi  9236  fodomfi  9347  imafiOLD  9351  domunfican  9358  fodomfiOLD  9367  f1opwfi  9393  fipreima  9395  marypha1lem  9470  ordtypelem2  9556  ordtypelem3  9557  ordtypelem9  9563  dfac12lem2  10182  dfac12r  10184  ackbij2lem2  10276  ackbij2lem3  10277  r1om  10280  enfin2i  10358  zorn2lem6  10538  zorn2lem7  10539  isacs5lem  18602  acsdrscl  18603  gicsubgen  19309  ghmqusnsglem1  19310  ghmquskerlem1  19313  ghmquskerco  19314  gicqusker  19318  efgrelexlema  19781  tgcn  23275  subbascn  23277  iscnp4  23286  cnpnei  23287  cnima  23288  iscncl  23292  cncls  23297  cnconst2  23306  cnrest2  23309  cnprest  23312  cnindis  23315  cncmp  23415  cmpfi  23431  2ndcomap  23481  ptbasfi  23604  xkoopn  23612  xkoccn  23642  txcnp  23643  ptcnplem  23644  txcnmpt  23647  ptrescn  23662  xkoco1cn  23680  xkoco2cn  23681  xkococn  23683  xkoinjcn  23710  elqtop  23720  qtopomap  23741  qtopcmap  23742  ordthmeolem  23824  fbasrn  23907  elfm  23970  elfm2  23971  elfm3  23973  imaelfm  23974  rnelfmlem  23975  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem3  23979  fmfnfmlem4  23980  fmco  23984  flffbas  24018  lmflf  24028  fcfneii  24060  ptcmplem3  24077  ptcmplem5  24079  ptcmpg  24080  cnextcn  24090  symgtgp  24129  ghmcnp  24138  eltsms  24156  tsmsf1o  24168  fmucnd  24316  ucnextcn  24328  metcnp3  24568  mbfdm  25674  ismbf  25676  mbfima  25678  ismbfd  25687  mbfimaopnlem  25703  mbfimaopn2  25705  i1fd  25729  ellimc2  25926  limcflf  25930  xrlimcnp  27025  oldval  27907  ubthlem1  30898  disjpreima  32603  imadifxp  32620  preimane  32686  fnpreimac  32687  lmicqusker  33425  ricqusker  33434  algextdeglem4  33725  algextdeg  33730  qtophaus  33796  rhmpreimacnlem  33844  rrhre  33983  mbfmcnvima  34236  imambfm  34243  eulerpartgbij  34353  erdszelem1  35175  erdsze  35186  erdsze2lem2  35188  cvmscbv  35242  cvmsi  35249  cvmsval  35250  cvmliftlem15  35282  opelco3  35755  brimageg  35908  fnimage  35910  imageval  35911  fvimage  35912  filnetlem4  36363  bj-imdirval3  37166  bj-imdirco  37172  ptrest  37605  ismtyhmeolem  37790  ismtybndlem  37792  heibor1lem  37795  zndvdchrrhm  41952  aks6d1c7lem2  42162  aks5lem4a  42171  lmhmfgima  43072  brtrclfv2  43716  csbfv12gALTVD  44896  icccncfext  45842  sge0f1o  46337  smfresal  46743  smfpimbor1lem1  46753  smfpimbor1lem2  46754  smfco  46757  f1cof1b  47026  fnfocofob  47028  imaelsetpreimafv  47319  fundcmpsurinjlem3  47324  imasetpreimafvbijlemfo  47329  fundcmpsurbijinjpreimafv  47331  isuspgrim0  47809  uspgrimprop  47810  isuspgrimlem  47811  grimco  47817  gricushgr  47823  grimedg  47840  grtrimap  47850  isubgr3stgrlem5  47872  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  isubgr3stgrlem8  47875  uspgrlimlem4  47893  grlimgrtrilem2  47897