Theorem imaeq2 6066

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 5981	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5932	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5671	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5671	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5659   ↾ cres 5660   “ cima 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-cnv 5666  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671

This theorem is used by:  imaeq2i  6068  imaeq2d  6070  relimasn  6101  cnvimassrndmOLD  6218  fimadmfo  6835  ssimaex  7001  ssimaexg  7002  isoselem  7380  isowe2  7389  f1opw2  7708  mptcnfimad  8032  fnse  8187  supp0cosupp0  8263  tz7.49  8493  ecexr  8760  fopwdom  9142  sbthlem2  9145  sbth  9154  ssenen  9208  sbthfi  9252  fodomfi  9342  domunfican  9351  f1opwfi  9383  fipreima  9385  marypha1lem  9462  ordtypelem2  9550  ordtypelem3  9551  ordtypelem9  9557  dfac12lem2  10262  dfac12r  10264  ackbij2lem2  10356  ackbij2lem3  10357  hfom  10360  enfin2i  10438  zorn2lem6  10618  zorn2lem7  10619  isacs5lem  18769  acsdrscl  18770  gicsubgen  19544  ghmqusnsglem1  19545  ghmquskerlem1  19548  ghmquskerco  19549  gicqusker  19553  efgrelexlema  20014  tgcn  23625  subbascn  23627  iscnp4  23636  cnpnei  23637  cnima  23638  iscncl  23642  cncls  23647  cnconst2  23656  cnrest2  23659  cnprest  23662  cnindis  23665  cncmp  23765  cmpfi  23781  2ndcomap  23832  ptbasfi  23955  xkoopn  23963  xkoccn  23993  txcnp  23994  ptcnplem  23995  txcnmpt  23998  ptrescn  24013  xkoco1cn  24031  xkoco2cn  24032  xkococn  24034  xkoinjcn  24061  elqtop  24071  qtopomap  24092  qtopcmap  24093  ordthmeolem  24175  fbasrn  24258  elfm  24321  elfm2  24322  elfm3  24324  imaelfm  24325  rnelfmlem  24326  rnelfm  24327  fmfnfmlem2  24329  fmfnfmlem3  24330  fmfnfmlem4  24331  fmco  24335  flffbas  24369  lmflf  24379  fcfneii  24411  ptcmplem3  24428  ptcmplem5  24430  ptcmpg  24431  cnextcn  24441  symgtgp  24480  ghmcnp  24489  eltsms  24507  tsmsf1o  24519  fmucnd  24665  ucnextcn  24677  metcnp3  24914  mbfdm  26002  ismbf  26004  mbfima  26006  ismbfd  26015  mbfimaopnlem  26031  mbfimaopn2  26033  i1fd  26057  ellimc2  26252  limcflf  26256  xrlimcnp  27353  oldval  28277  ubthlem1  31529  disjpreima  33276  imadifxp  33293  preimane  33361  fnpreimac  33362  lmicqusker  34073  ricqusker  34081  algextdeglem4  34463  algextdeg  34468  qtophaus  34579  rhmpreimacnlem  34627  rrhre  34764  mbfmcnvima  34999  imambfm  35005  eulerpartgbij  35115  erdszelem1  36164  erdsze  36175  erdsze2lem2  36177  cvmscbv  36231  cvmsi  36238  cvmsval  36239  cvmliftlem15  36271  opelco3  36754  brimageg  36904  fnimage  36906  imageval  36907  fvimage  36908  filnetlem4  37384  bj-imdirval3  38373  bj-imdirco  38379  ptrest  38805  ismtyhmeolem  39004  ismtybndlem  39006  heibor1lem  39009  zndvdchrrhm  43289  aks6d1c7lem2  43497  aks5lem4a  43506  lmhmfgima  44352  brtrclfv2  44988  csbfv12gALTVD  46141  ackbij3  46289  icccncfext  47170  sge0f1o  47665  smfresal  48071  smfpimbor1lem1  48081  smfpimbor1lem2  48082  smfco  48085  f1cof1b  48420  fnfocofob  48422  imaelsetpreimafv  48750  fundcmpsurinjlem3  48755  imasetpreimafvbijlemfo  48760  fundcmpsurbijinjpreimafv  48762  grimco  49260  uhgrimedgi  49261  isuspgrim0  49265  isuspgrimlem  49266  upgrimwlklem5  49272  gricushgr  49288  grimedg  49306  grtrimap  49319  isubgr3stgrlem5  49341  isubgr3stgrlem6  49342  isubgr3stgrlem7  49343  isubgr3stgrlem8  49344  uspgrlimlem4  49362  grlimedgclnbgr  49366  grlimgrtrilem2  49373