Theorem imaeq2 6055

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

Syntax hints:   → wi 4   = wceq 1541  ran crn 5677   ↾ cres 5678   “ cima 5679

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689

This theorem is referenced by:  imaeq2i  6057  imaeq2d  6059  relimasn  6083  cnvimassrndm  6151  funimaexgOLD  6635  fimadmfo  6814  ssimaex  6976  ssimaexg  6977  isoselem  7337  isowe2  7346  f1opw2  7660  fnse  8118  supp0cosupp0  8192  tz7.49  8444  ecexr  8707  fopwdom  9079  sbthlem2  9083  sbth  9092  ssenen  9150  imafi  9174  sbthfi  9201  domunfican  9319  fodomfi  9324  f1opwfi  9355  fipreima  9357  marypha1lem  9427  ordtypelem2  9513  ordtypelem3  9514  ordtypelem9  9520  dfac12lem2  10138  dfac12r  10140  ackbij2lem2  10234  ackbij2lem3  10235  r1om  10238  enfin2i  10315  zorn2lem6  10495  zorn2lem7  10496  isacs5lem  18497  acsdrscl  18498  gicsubgen  19151  efgrelexlema  19616  tgcn  22755  subbascn  22757  iscnp4  22766  cnpnei  22767  cnima  22768  iscncl  22772  cncls  22777  cnconst2  22786  cnrest2  22789  cnprest  22792  cnindis  22795  cncmp  22895  cmpfi  22911  2ndcomap  22961  ptbasfi  23084  xkoopn  23092  xkoccn  23122  txcnp  23123  ptcnplem  23124  txcnmpt  23127  ptrescn  23142  xkoco1cn  23160  xkoco2cn  23161  xkococn  23163  xkoinjcn  23190  elqtop  23200  qtopomap  23221  qtopcmap  23222  ordthmeolem  23304  fbasrn  23387  elfm  23450  elfm2  23451  elfm3  23453  imaelfm  23454  rnelfmlem  23455  rnelfm  23456  fmfnfmlem2  23458  fmfnfmlem3  23459  fmfnfmlem4  23460  fmco  23464  flffbas  23498  lmflf  23508  fcfneii  23540  ptcmplem3  23557  ptcmplem5  23559  ptcmpg  23560  cnextcn  23570  symgtgp  23609  ghmcnp  23618  eltsms  23636  tsmsf1o  23648  fmucnd  23796  ucnextcn  23808  metcnp3  24048  mbfdm  25142  ismbf  25144  mbfima  25146  ismbfd  25155  mbfimaopnlem  25171  mbfimaopn2  25173  i1fd  25197  ellimc2  25393  limcflf  25397  xrlimcnp  26470  oldval  27346  ubthlem1  30118  disjpreima  31810  imadifxp  31827  preimane  31890  fnpreimac  31891  ghmquskerlem1  32523  ghmquskerco  32524  gicqusker  32528  lmicqusker  32530  ricqusker  32540  algextdeglem1  32767  qtophaus  32811  rhmpreimacnlem  32859  rrhre  32996  mbfmcnvima  33249  imambfm  33256  eulerpartgbij  33366  erdszelem1  34177  erdsze  34188  erdsze2lem2  34190  cvmscbv  34244  cvmsi  34251  cvmsval  34252  cvmliftlem15  34284  opelco3  34741  brimageg  34894  fnimage  34896  imageval  34897  fvimage  34898  filnetlem4  35261  bj-imdirval3  36060  bj-imdirco  36066  ptrest  36482  ismtyhmeolem  36667  ismtybndlem  36669  heibor1lem  36672  lmhmfgima  41816  brtrclfv2  42468  csbfv12gALTVD  43650  icccncfext  44593  sge0f1o  45088  smfresal  45494  smfpimbor1lem1  45504  smfpimbor1lem2  45505  smfco  45508  f1cof1b  45775  fnfocofob  45777  imaelsetpreimafv  46053  fundcmpsurinjlem3  46058  imasetpreimafvbijlemfo  46063  fundcmpsurbijinjpreimafv  46065  isomushgr  46484  isomuspgrlem1  46485  isomuspgrlem2a  46486  isomuspgrlem2b  46487  isomuspgrlem2c  46488  isomuspgrlem2d  46489  isomuspgr  46492  isomgrsym  46494