Theorem imaeq2 6048

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 5965	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5920	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5664	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5664	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5652   ↾ cres 5653   “ cima 5654

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  imaeq2i  6050  imaeq2d  6052  relimasn  6083  cnvimassrndmOLD  6198  fimadmfo  6803  ssimaex  6968  ssimaexg  6969  isoselem  7347  isowe2  7356  f1opw2  7674  mptcnfimad  7996  fnse  8143  supp0cosupp0  8218  tz7.49  8448  ecexr  8715  fopwdom  9097  sbthlem2  9100  sbth  9109  ssenen  9163  sbthfi  9207  fodomfi  9297  domunfican  9306  f1opwfi  9338  fipreima  9340  marypha1lem  9418  ordtypelem2  9506  ordtypelem3  9507  ordtypelem9  9513  dfac12lem2  10216  dfac12r  10218  ackbij2lem2  10310  ackbij2lem3  10311  hfom  10314  enfin2i  10392  zorn2lem6  10572  zorn2lem7  10573  isacs5lem  18712  acsdrscl  18713  gicsubgen  19486  ghmqusnsglem1  19487  ghmquskerlem1  19490  ghmquskerco  19491  gicqusker  19495  efgrelexlema  19956  tgcn  23563  subbascn  23565  iscnp4  23574  cnpnei  23575  cnima  23576  iscncl  23580  cncls  23585  cnconst2  23594  cnrest2  23597  cnprest  23600  cnindis  23603  cncmp  23703  cmpfi  23719  2ndcomap  23770  ptbasfi  23893  xkoopn  23901  xkoccn  23931  txcnp  23932  ptcnplem  23933  txcnmpt  23936  ptrescn  23951  xkoco1cn  23969  xkoco2cn  23970  xkococn  23972  xkoinjcn  23999  elqtop  24009  qtopomap  24030  qtopcmap  24031  ordthmeolem  24113  fbasrn  24196  elfm  24259  elfm2  24260  elfm3  24262  imaelfm  24263  rnelfmlem  24264  rnelfm  24265  fmfnfmlem2  24267  fmfnfmlem3  24268  fmfnfmlem4  24269  fmco  24273  flffbas  24307  lmflf  24317  fcfneii  24349  ptcmplem3  24366  ptcmplem5  24368  ptcmpg  24369  cnextcn  24379  symgtgp  24418  ghmcnp  24427  eltsms  24445  tsmsf1o  24457  fmucnd  24603  ucnextcn  24615  metcnp3  24852  mbfdm  25940  ismbf  25942  mbfima  25944  ismbfd  25953  mbfimaopnlem  25969  mbfimaopn2  25971  i1fd  25995  ellimc2  26190  limcflf  26194  xrlimcnp  27289  oldval  28213  ubthlem1  31465  disjpreima  33171  imadifxp  33188  preimane  33256  fnpreimac  33257  lmicqusker  33962  ricqusker  33970  algextdeglem4  34345  algextdeg  34350  qtophaus  34461  rhmpreimacnlem  34509  rrhre  34646  mbfmcnvima  34881  imambfm  34887  eulerpartgbij  34997  erdszelem1  35935  erdsze  35946  erdsze2lem2  35948  cvmscbv  36002  cvmsi  36009  cvmsval  36010  cvmliftlem15  36042  opelco3  36519  brimageg  36669  fnimage  36671  imageval  36672  fvimage  36673  filnetlem4  37149  bj-imdirval3  38085  bj-imdirco  38091  ptrest  38517  ismtyhmeolem  38718  ismtybndlem  38720  heibor1lem  38723  zndvdchrrhm  43003  aks6d1c7lem2  43211  aks5lem4a  43220  lmhmfgima  44070  brtrclfv2  44712  csbfv12gALTVD  45866  icccncfext  46866  sge0f1o  47361  smfresal  47767  smfpimbor1lem1  47777  smfpimbor1lem2  47778  smfco  47781  f1cof1b  48116  fnfocofob  48118  imaelsetpreimafv  48446  fundcmpsurinjlem3  48451  imasetpreimafvbijlemfo  48456  fundcmpsurbijinjpreimafv  48458  grimco  48956  uhgrimedgi  48957  isuspgrim0  48961  isuspgrimlem  48962  upgrimwlklem5  48968  gricushgr  48984  grimedg  49002  grtrimap  49015  isubgr3stgrlem5  49037  isubgr3stgrlem6  49038  isubgr3stgrlem7  49039  isubgr3stgrlem8  49040  uspgrlimlem4  49058  grlimedgclnbgr  49062  grlimgrtrilem2  49069