Theorem imaeq2 6045

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 5960	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5914	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5660	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5660	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2822	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1560  ran crn 5648   ↾ cres 5649   “ cima 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-cnv 5655  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660

This theorem is referenced by:  imaeq2i  6047  imaeq2d  6049  relimasn  6074  cnvimassrndm  6137  fimadmfo  6787  ssimaex  6952  ssimaexg  6953  isoselem  7325  isowe2  7334  f1opw2  7651  mptcnfimad  7967  fnse  8113  supp0cosupp0  8188  tz7.49  8416  ecexr  8683  fopwdom  9057  sbthlem2  9060  sbth  9069  ssenen  9123  sbthfi  9167  fodomfi  9256  imafiOLD  9260  domunfican  9266  f1opwfi  9299  fipreima  9301  marypha1lem  9379  ordtypelem2  9467  ordtypelem3  9468  ordtypelem9  9474  dfac12lem2  10101  dfac12r  10103  ackbij2lem2  10195  ackbij2lem3  10196  r1om  10199  enfin2i  10278  zorn2lem6  10458  zorn2lem7  10459  isacs5lem  18577  acsdrscl  18578  gicsubgen  19319  ghmqusnsglem1  19320  ghmquskerlem1  19323  ghmquskerco  19324  gicqusker  19328  efgrelexlema  19789  tgcn  23309  subbascn  23311  iscnp4  23320  cnpnei  23321  cnima  23322  iscncl  23326  cncls  23331  cnconst2  23340  cnrest2  23343  cnprest  23346  cnindis  23349  cncmp  23449  cmpfi  23465  2ndcomap  23515  ptbasfi  23638  xkoopn  23646  xkoccn  23676  txcnp  23677  ptcnplem  23678  txcnmpt  23681  ptrescn  23696  xkoco1cn  23714  xkoco2cn  23715  xkococn  23717  xkoinjcn  23744  elqtop  23754  qtopomap  23775  qtopcmap  23776  ordthmeolem  23858  fbasrn  23941  elfm  24004  elfm2  24005  elfm3  24007  imaelfm  24008  rnelfmlem  24009  rnelfm  24010  fmfnfmlem2  24012  fmfnfmlem3  24013  fmfnfmlem4  24014  fmco  24018  flffbas  24052  lmflf  24062  fcfneii  24094  ptcmplem3  24111  ptcmplem5  24113  ptcmpg  24114  cnextcn  24124  symgtgp  24163  ghmcnp  24172  eltsms  24190  tsmsf1o  24202  fmucnd  24348  ucnextcn  24360  metcnp3  24597  mbfdm  25685  ismbf  25687  mbfima  25689  ismbfd  25698  mbfimaopnlem  25714  mbfimaopn2  25716  i1fd  25740  ellimc2  25936  limcflf  25940  xrlimcnp  27030  oldval  27924  ubthlem1  31070  disjpreima  32781  imadifxp  32798  preimane  32868  fnpreimac  32869  lmicqusker  33601  ricqusker  33610  algextdeglem4  34014  algextdeg  34019  qtophaus  34130  rhmpreimacnlem  34178  rrhre  34315  mbfmcnvima  34549  imambfm  34556  eulerpartgbij  34666  erdszelem1  35538  erdsze  35549  erdsze2lem2  35551  cvmscbv  35605  cvmsi  35612  cvmsval  35613  cvmliftlem15  35645  opelco3  36122  brimageg  36272  fnimage  36274  imageval  36275  fvimage  36276  filnetlem4  36738  bj-imdirval3  37673  bj-imdirco  37679  ptrest  38115  ismtyhmeolem  38300  ismtybndlem  38302  heibor1lem  38305  zndvdchrrhm  42587  aks6d1c7lem2  42795  aks5lem4a  42804  lmhmfgima  43658  brtrclfv2  44300  csbfv12gALTVD  45471  icccncfext  46458  sge0f1o  46953  smfresal  47359  smfpimbor1lem1  47369  smfpimbor1lem2  47370  smfco  47373  f1cof1b  47668  fnfocofob  47670  imaelsetpreimafv  47998  fundcmpsurinjlem3  48003  imasetpreimafvbijlemfo  48008  fundcmpsurbijinjpreimafv  48010  grimco  48508  uhgrimedgi  48509  isuspgrim0  48513  isuspgrimlem  48514  upgrimwlklem5  48520  gricushgr  48536  grimedg  48554  grtrimap  48567  isubgr3stgrlem5  48589  isubgr3stgrlem6  48590  isubgr3stgrlem7  48591  isubgr3stgrlem8  48592  uspgrlimlem4  48610  grlimedgclnbgr  48614  grlimgrtrilem2  48621