Theorem imaeq2 6008

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631

This theorem is referenced by:  imaeq2i  6010  imaeq2d  6012  relimasn  6037  cnvimassrndm  6103  fimadmfo  6748  ssimaex  6912  ssimaexg  6913  isoselem  7285  isowe2  7294  f1opw2  7611  mptcnfimad  7928  fnse  8073  supp0cosupp0  8148  tz7.49  8374  ecexr  8638  fopwdom  9013  sbthlem2  9016  sbth  9025  ssenen  9079  sbthfi  9123  fodomfi  9212  imafiOLD  9216  domunfican  9222  fodomfiOLD  9230  f1opwfi  9256  fipreima  9258  marypha1lem  9336  ordtypelem2  9424  ordtypelem3  9425  ordtypelem9  9431  dfac12lem2  10058  dfac12r  10060  ackbij2lem2  10152  ackbij2lem3  10153  r1om  10156  enfin2i  10234  zorn2lem6  10414  zorn2lem7  10415  isacs5lem  18502  acsdrscl  18503  gicsubgen  19245  ghmqusnsglem1  19246  ghmquskerlem1  19249  ghmquskerco  19250  gicqusker  19254  efgrelexlema  19715  tgcn  23235  subbascn  23237  iscnp4  23246  cnpnei  23247  cnima  23248  iscncl  23252  cncls  23257  cnconst2  23266  cnrest2  23269  cnprest  23272  cnindis  23275  cncmp  23375  cmpfi  23391  2ndcomap  23441  ptbasfi  23564  xkoopn  23572  xkoccn  23602  txcnp  23603  ptcnplem  23604  txcnmpt  23607  ptrescn  23622  xkoco1cn  23640  xkoco2cn  23641  xkococn  23643  xkoinjcn  23670  elqtop  23680  qtopomap  23701  qtopcmap  23702  ordthmeolem  23784  fbasrn  23867  elfm  23930  elfm2  23931  elfm3  23933  imaelfm  23934  rnelfmlem  23935  rnelfm  23936  fmfnfmlem2  23938  fmfnfmlem3  23939  fmfnfmlem4  23940  fmco  23944  flffbas  23978  lmflf  23988  fcfneii  24020  ptcmplem3  24037  ptcmplem5  24039  ptcmpg  24040  cnextcn  24050  symgtgp  24089  ghmcnp  24098  eltsms  24116  tsmsf1o  24128  fmucnd  24274  ucnextcn  24286  metcnp3  24523  mbfdm  25611  ismbf  25613  mbfima  25615  ismbfd  25624  mbfimaopnlem  25640  mbfimaopn2  25642  i1fd  25666  ellimc2  25862  limcflf  25866  xrlimcnp  26950  oldval  27844  ubthlem1  30959  disjpreima  32673  imadifxp  32690  preimane  32761  fnpreimac  32762  lmicqusker  33501  ricqusker  33510  algextdeglem4  33904  algextdeg  33909  qtophaus  34020  rhmpreimacnlem  34068  rrhre  34205  mbfmcnvima  34439  imambfm  34446  eulerpartgbij  34556  erdszelem1  35419  erdsze  35430  erdsze2lem2  35432  cvmscbv  35486  cvmsi  35493  cvmsval  35494  cvmliftlem15  35526  opelco3  36003  brimageg  36153  fnimage  36155  imageval  36156  fvimage  36157  filnetlem4  36609  bj-imdirval3  37544  bj-imdirco  37550  ptrest  37986  ismtyhmeolem  38171  ismtybndlem  38173  heibor1lem  38176  zndvdchrrhm  42458  aks6d1c7lem2  42666  aks5lem4a  42675  lmhmfgima  43529  brtrclfv2  44171  csbfv12gALTVD  45342  icccncfext  46330  sge0f1o  46825  smfresal  47231  smfpimbor1lem1  47241  smfpimbor1lem2  47242  smfco  47245  f1cof1b  47540  fnfocofob  47542  imaelsetpreimafv  47870  fundcmpsurinjlem3  47875  imasetpreimafvbijlemfo  47880  fundcmpsurbijinjpreimafv  47882  grimco  48380  uhgrimedgi  48381  isuspgrim0  48385  isuspgrimlem  48386  upgrimwlklem5  48392  gricushgr  48408  grimedg  48426  grtrimap  48439  isubgr3stgrlem5  48461  isubgr3stgrlem6  48462  isubgr3stgrlem7  48463  isubgr3stgrlem8  48464  uspgrlimlem4  48482  grlimedgclnbgr  48486  grlimgrtrilem2  48493