Theorem imaeq2 5925

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 5848	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5808	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5568	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5568	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2881	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1537  ran crn 5556   ↾ cres 5557   “ cima 5558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568

This theorem is referenced by:  imaeq2i  5927  imaeq2d  5929  relimasn  5952  funimaexg  6440  fimadmfo  6599  ssimaex  6748  ssimaexg  6749  isoselem  7094  isowe2  7103  f1opw2  7400  fnse  7827  supp0cosupp0  7872  supp0cosupp0OLD  7873  tz7.49  8081  ecexr  8294  fopwdom  8625  sbthlem2  8628  sbth  8637  ssenen  8691  domunfican  8791  fodomfi  8797  f1opwfi  8828  fipreima  8830  marypha1lem  8897  ordtypelem2  8983  ordtypelem3  8984  ordtypelem9  8990  dfac12lem2  9570  dfac12r  9572  ackbij2lem2  9662  ackbij2lem3  9663  r1om  9666  enfin2i  9743  zorn2lem6  9923  zorn2lem7  9924  isacs5lem  17779  acsdrscl  17780  gicsubgen  18418  efgrelexlema  18875  tgcn  21860  subbascn  21862  iscnp4  21871  cnpnei  21872  cnima  21873  iscncl  21877  cncls  21882  cnconst2  21891  cnrest2  21894  cnprest  21897  cnindis  21900  cncmp  22000  cmpfi  22016  2ndcomap  22066  ptbasfi  22189  xkoopn  22197  xkoccn  22227  txcnp  22228  ptcnplem  22229  txcnmpt  22232  ptrescn  22247  xkoco1cn  22265  xkoco2cn  22266  xkococn  22268  xkoinjcn  22295  elqtop  22305  qtopomap  22326  qtopcmap  22327  ordthmeolem  22409  fbasrn  22492  elfm  22555  elfm2  22556  elfm3  22558  imaelfm  22559  rnelfmlem  22560  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem3  22564  fmfnfmlem4  22565  fmco  22569  flffbas  22603  lmflf  22613  fcfneii  22645  ptcmplem3  22662  ptcmplem5  22664  ptcmpg  22665  cnextcn  22675  symgtgp  22714  ghmcnp  22723  eltsms  22741  tsmsf1o  22753  fmucnd  22901  ucnextcn  22913  metcnp3  23150  mbfdm  24227  ismbf  24229  mbfima  24231  ismbfd  24240  mbfimaopnlem  24256  mbfimaopn2  24258  i1fd  24282  ellimc2  24475  limcflf  24479  xrlimcnp  25546  ubthlem1  28647  disjpreima  30334  imadifxp  30351  preimane  30415  fnpreimac  30416  qtophaus  31100  rrhre  31262  mbfmcnvima  31515  imambfm  31520  eulerpartgbij  31630  erdszelem1  32438  erdsze  32449  erdsze2lem2  32451  cvmscbv  32505  cvmsi  32512  cvmsval  32513  cvmliftlem15  32545  opelco3  33018  brimageg  33388  fnimage  33390  imageval  33391  fvimage  33392  filnetlem4  33729  bj-imdirval3  34477  ptrest  34906  ismtyhmeolem  35097  ismtybndlem  35099  heibor1lem  35102  lmhmfgima  39733  brtrclfv2  40121  csbfv12gALTVD  41282  icccncfext  42219  sge0f1o  42713  smfresal  43112  smfpimbor1lem1  43122  smfpimbor1lem2  43123  smfco  43126  imaelsetpreimafv  43604  fundcmpsurinjlem3  43609  imasetpreimafvbijlemfo  43614  fundcmpsurbijinjpreimafv  43616  isomushgr  44040  isomuspgrlem1  44041  isomuspgrlem2a  44042  isomuspgrlem2b  44043  isomuspgrlem2c  44044  isomuspgrlem2d  44045  isomuspgr  44048  isomgrsym  44050