Theorem imaeq2 6016

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 5934	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5888	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5638	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5638	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1542  ran crn 5626   ↾ cres 5627   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  imaeq2i  6018  imaeq2d  6020  relimasn  6045  cnvimassrndm  6111  fimadmfo  6756  ssimaex  6920  ssimaexg  6921  isoselem  7290  isowe2  7299  f1opw2  7616  mptcnfimad  7933  fnse  8077  supp0cosupp0  8152  tz7.49  8378  ecexr  8642  fopwdom  9017  sbthlem2  9020  sbth  9029  ssenen  9083  sbthfi  9127  fodomfi  9216  imafiOLD  9220  domunfican  9226  fodomfiOLD  9234  f1opwfi  9260  fipreima  9262  marypha1lem  9340  ordtypelem2  9428  ordtypelem3  9429  ordtypelem9  9435  dfac12lem2  10061  dfac12r  10063  ackbij2lem2  10155  ackbij2lem3  10156  r1om  10159  enfin2i  10237  zorn2lem6  10417  zorn2lem7  10418  isacs5lem  18505  acsdrscl  18506  gicsubgen  19248  ghmqusnsglem1  19249  ghmquskerlem1  19252  ghmquskerco  19253  gicqusker  19257  efgrelexlema  19718  tgcn  23230  subbascn  23232  iscnp4  23241  cnpnei  23242  cnima  23243  iscncl  23247  cncls  23252  cnconst2  23261  cnrest2  23264  cnprest  23267  cnindis  23270  cncmp  23370  cmpfi  23386  2ndcomap  23436  ptbasfi  23559  xkoopn  23567  xkoccn  23597  txcnp  23598  ptcnplem  23599  txcnmpt  23602  ptrescn  23617  xkoco1cn  23635  xkoco2cn  23636  xkococn  23638  xkoinjcn  23665  elqtop  23675  qtopomap  23696  qtopcmap  23697  ordthmeolem  23779  fbasrn  23862  elfm  23925  elfm2  23926  elfm3  23928  imaelfm  23929  rnelfmlem  23930  rnelfm  23931  fmfnfmlem2  23933  fmfnfmlem3  23934  fmfnfmlem4  23935  fmco  23939  flffbas  23973  lmflf  23983  fcfneii  24015  ptcmplem3  24032  ptcmplem5  24034  ptcmpg  24035  cnextcn  24045  symgtgp  24084  ghmcnp  24093  eltsms  24111  tsmsf1o  24123  fmucnd  24269  ucnextcn  24281  metcnp3  24518  mbfdm  25606  ismbf  25608  mbfima  25610  ismbfd  25619  mbfimaopnlem  25635  mbfimaopn2  25637  i1fd  25661  ellimc2  25857  limcflf  25861  xrlimcnp  26948  oldval  27843  ubthlem1  30959  disjpreima  32672  imadifxp  32689  preimane  32760  fnpreimac  32761  lmicqusker  33496  ricqusker  33505  algextdeglem4  33883  algextdeg  33888  qtophaus  33999  rhmpreimacnlem  34047  rrhre  34184  mbfmcnvima  34418  imambfm  34425  eulerpartgbij  34535  erdszelem1  35392  erdsze  35403  erdsze2lem2  35405  cvmscbv  35459  cvmsi  35466  cvmsval  35467  cvmliftlem15  35499  opelco3  35976  brimageg  36126  fnimage  36128  imageval  36129  fvimage  36130  filnetlem4  36582  bj-imdirval3  37517  bj-imdirco  37523  ptrest  37957  ismtyhmeolem  38142  ismtybndlem  38144  heibor1lem  38147  zndvdchrrhm  42429  aks6d1c7lem2  42637  aks5lem4a  42646  lmhmfgima  43533  brtrclfv2  44175  csbfv12gALTVD  45346  icccncfext  46336  sge0f1o  46831  smfresal  47237  smfpimbor1lem1  47247  smfpimbor1lem2  47248  smfco  47251  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