Theorem imaeq2 5954

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 5875	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5836	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5593	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5593	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1539  ran crn 5581   ↾ cres 5582   “ cima 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593

This theorem is referenced by:  imaeq2i  5956  imaeq2d  5958  relimasn  5981  cnvimassrndm  6044  funimaexg  6504  fimadmfo  6681  ssimaex  6835  ssimaexg  6836  isoselem  7192  isowe2  7201  f1opw2  7502  fnse  7945  supp0cosupp0  7995  tz7.49  8246  ecexr  8461  fopwdom  8820  sbthlem2  8824  sbth  8833  ssenen  8887  imafi  8920  sbthfi  8942  domunfican  9017  fodomfi  9022  f1opwfi  9053  fipreima  9055  marypha1lem  9122  ordtypelem2  9208  ordtypelem3  9209  ordtypelem9  9215  dfac12lem2  9831  dfac12r  9833  ackbij2lem2  9927  ackbij2lem3  9928  r1om  9931  enfin2i  10008  zorn2lem6  10188  zorn2lem7  10189  isacs5lem  18178  acsdrscl  18179  gicsubgen  18809  efgrelexlema  19270  tgcn  22311  subbascn  22313  iscnp4  22322  cnpnei  22323  cnima  22324  iscncl  22328  cncls  22333  cnconst2  22342  cnrest2  22345  cnprest  22348  cnindis  22351  cncmp  22451  cmpfi  22467  2ndcomap  22517  ptbasfi  22640  xkoopn  22648  xkoccn  22678  txcnp  22679  ptcnplem  22680  txcnmpt  22683  ptrescn  22698  xkoco1cn  22716  xkoco2cn  22717  xkococn  22719  xkoinjcn  22746  elqtop  22756  qtopomap  22777  qtopcmap  22778  ordthmeolem  22860  fbasrn  22943  elfm  23006  elfm2  23007  elfm3  23009  imaelfm  23010  rnelfmlem  23011  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem3  23015  fmfnfmlem4  23016  fmco  23020  flffbas  23054  lmflf  23064  fcfneii  23096  ptcmplem3  23113  ptcmplem5  23115  ptcmpg  23116  cnextcn  23126  symgtgp  23165  ghmcnp  23174  eltsms  23192  tsmsf1o  23204  fmucnd  23352  ucnextcn  23364  metcnp3  23602  mbfdm  24695  ismbf  24697  mbfima  24699  ismbfd  24708  mbfimaopnlem  24724  mbfimaopn2  24726  i1fd  24750  ellimc2  24946  limcflf  24950  xrlimcnp  26023  ubthlem1  29133  disjpreima  30824  imadifxp  30841  preimane  30909  fnpreimac  30910  qtophaus  31688  rhmpreimacnlem  31736  rrhre  31871  mbfmcnvima  32124  imambfm  32129  eulerpartgbij  32239  erdszelem1  33053  erdsze  33064  erdsze2lem2  33066  cvmscbv  33120  cvmsi  33127  cvmsval  33128  cvmliftlem15  33160  opelco3  33655  oldval  33965  brimageg  34156  fnimage  34158  imageval  34159  fvimage  34160  filnetlem4  34497  bj-imdirval3  35282  bj-imdirco  35288  ptrest  35703  ismtyhmeolem  35889  ismtybndlem  35891  heibor1lem  35894  lmhmfgima  40825  brtrclfv2  41224  csbfv12gALTVD  42408  icccncfext  43318  sge0f1o  43810  smfresal  44209  smfpimbor1lem1  44219  smfpimbor1lem2  44220  smfco  44223  f1cof1b  44456  fnfocofob  44458  imaelsetpreimafv  44735  fundcmpsurinjlem3  44740  imasetpreimafvbijlemfo  44745  fundcmpsurbijinjpreimafv  44747  isomushgr  45166  isomuspgrlem1  45167  isomuspgrlem2a  45168  isomuspgrlem2b  45169  isomuspgrlem2c  45170  isomuspgrlem2d  45171  isomuspgr  45174  isomgrsym  45176