Theorem imaeq2 6007

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5620   ↾ cres 5621   “ cima 5622

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  imaeq2i  6009  imaeq2d  6011  relimasn  6036  cnvimassrndm  6101  fimadmfo  6745  ssimaex  6908  ssimaexg  6909  isoselem  7278  isowe2  7287  f1opw2  7604  mptcnfimad  7921  fnse  8066  supp0cosupp0  8141  tz7.49  8367  ecexr  8630  fopwdom  9002  sbthlem2  9005  sbth  9014  ssenen  9068  sbthfi  9113  fodomfi  9201  imafiOLD  9205  domunfican  9211  fodomfiOLD  9220  f1opwfi  9246  fipreima  9248  marypha1lem  9323  ordtypelem2  9411  ordtypelem3  9412  ordtypelem9  9418  dfac12lem2  10039  dfac12r  10041  ackbij2lem2  10133  ackbij2lem3  10134  r1om  10137  enfin2i  10215  zorn2lem6  10395  zorn2lem7  10396  isacs5lem  18451  acsdrscl  18452  gicsubgen  19158  ghmqusnsglem1  19159  ghmquskerlem1  19162  ghmquskerco  19163  gicqusker  19167  efgrelexlema  19628  tgcn  23137  subbascn  23139  iscnp4  23148  cnpnei  23149  cnima  23150  iscncl  23154  cncls  23159  cnconst2  23168  cnrest2  23171  cnprest  23174  cnindis  23177  cncmp  23277  cmpfi  23293  2ndcomap  23343  ptbasfi  23466  xkoopn  23474  xkoccn  23504  txcnp  23505  ptcnplem  23506  txcnmpt  23509  ptrescn  23524  xkoco1cn  23542  xkoco2cn  23543  xkococn  23545  xkoinjcn  23572  elqtop  23582  qtopomap  23603  qtopcmap  23604  ordthmeolem  23686  fbasrn  23769  elfm  23832  elfm2  23833  elfm3  23835  imaelfm  23836  rnelfmlem  23837  rnelfm  23838  fmfnfmlem2  23840  fmfnfmlem3  23841  fmfnfmlem4  23842  fmco  23846  flffbas  23880  lmflf  23890  fcfneii  23922  ptcmplem3  23939  ptcmplem5  23941  ptcmpg  23942  cnextcn  23952  symgtgp  23991  ghmcnp  24000  eltsms  24018  tsmsf1o  24030  fmucnd  24177  ucnextcn  24189  metcnp3  24426  mbfdm  25525  ismbf  25527  mbfima  25529  ismbfd  25538  mbfimaopnlem  25554  mbfimaopn2  25556  i1fd  25580  ellimc2  25776  limcflf  25780  xrlimcnp  26876  oldval  27764  ubthlem1  30814  disjpreima  32528  imadifxp  32545  preimane  32613  fnpreimac  32614  lmicqusker  33355  ricqusker  33364  algextdeglem4  33687  algextdeg  33692  qtophaus  33803  rhmpreimacnlem  33851  rrhre  33988  mbfmcnvima  34223  imambfm  34230  eulerpartgbij  34340  erdszelem1  35164  erdsze  35175  erdsze2lem2  35177  cvmscbv  35231  cvmsi  35238  cvmsval  35239  cvmliftlem15  35271  opelco3  35748  brimageg  35901  fnimage  35903  imageval  35904  fvimage  35905  filnetlem4  36355  bj-imdirval3  37158  bj-imdirco  37164  ptrest  37599  ismtyhmeolem  37784  ismtybndlem  37786  heibor1lem  37789  zndvdchrrhm  41945  aks6d1c7lem2  42154  aks5lem4a  42163  lmhmfgima  43057  brtrclfv2  43700  csbfv12gALTVD  44872  icccncfext  45868  sge0f1o  46363  smfresal  46769  smfpimbor1lem1  46779  smfpimbor1lem2  46780  smfco  46783  f1cof1b  47061  fnfocofob  47063  imaelsetpreimafv  47379  fundcmpsurinjlem3  47384  imasetpreimafvbijlemfo  47389  fundcmpsurbijinjpreimafv  47391  grimco  47873  uhgrimedgi  47874  isuspgrim0  47878  isuspgrimlem  47879  upgrimwlklem5  47885  gricushgr  47901  grimedg  47919  grtrimap  47932  isubgr3stgrlem5  47954  isubgr3stgrlem6  47955  isubgr3stgrlem7  47956  isubgr3stgrlem8  47957  uspgrlimlem4  47975  grlimedgclnbgr  47979  grlimgrtrilem2  47986