Theorem imaeq2 6023

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

Syntax hints:   → wi 4   = wceq 1542  ran crn 5633   ↾ cres 5634   “ cima 5635

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  imaeq2i  6025  imaeq2d  6027  relimasn  6052  cnvimassrndm  6118  fimadmfo  6763  ssimaex  6927  ssimaexg  6928  isoselem  7297  isowe2  7306  f1opw2  7623  mptcnfimad  7940  fnse  8085  supp0cosupp0  8160  tz7.49  8386  ecexr  8650  fopwdom  9025  sbthlem2  9028  sbth  9037  ssenen  9091  sbthfi  9135  fodomfi  9224  imafiOLD  9228  domunfican  9234  fodomfiOLD  9242  f1opwfi  9268  fipreima  9270  marypha1lem  9348  ordtypelem2  9436  ordtypelem3  9437  ordtypelem9  9443  dfac12lem2  10067  dfac12r  10069  ackbij2lem2  10161  ackbij2lem3  10162  r1om  10165  enfin2i  10243  zorn2lem6  10423  zorn2lem7  10424  isacs5lem  18480  acsdrscl  18481  gicsubgen  19220  ghmqusnsglem1  19221  ghmquskerlem1  19224  ghmquskerco  19225  gicqusker  19229  efgrelexlema  19690  tgcn  23208  subbascn  23210  iscnp4  23219  cnpnei  23220  cnima  23221  iscncl  23225  cncls  23230  cnconst2  23239  cnrest2  23242  cnprest  23245  cnindis  23248  cncmp  23348  cmpfi  23364  2ndcomap  23414  ptbasfi  23537  xkoopn  23545  xkoccn  23575  txcnp  23576  ptcnplem  23577  txcnmpt  23580  ptrescn  23595  xkoco1cn  23613  xkoco2cn  23614  xkococn  23616  xkoinjcn  23643  elqtop  23653  qtopomap  23674  qtopcmap  23675  ordthmeolem  23757  fbasrn  23840  elfm  23903  elfm2  23904  elfm3  23906  imaelfm  23907  rnelfmlem  23908  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem3  23912  fmfnfmlem4  23913  fmco  23917  flffbas  23951  lmflf  23961  fcfneii  23993  ptcmplem3  24010  ptcmplem5  24012  ptcmpg  24013  cnextcn  24023  symgtgp  24062  ghmcnp  24071  eltsms  24089  tsmsf1o  24101  fmucnd  24247  ucnextcn  24259  metcnp3  24496  mbfdm  25595  ismbf  25597  mbfima  25599  ismbfd  25608  mbfimaopnlem  25624  mbfimaopn2  25626  i1fd  25650  ellimc2  25846  limcflf  25850  xrlimcnp  26946  oldval  27842  ubthlem1  30958  disjpreima  32671  imadifxp  32688  preimane  32759  fnpreimac  32760  lmicqusker  33511  ricqusker  33520  algextdeglem4  33898  algextdeg  33903  qtophaus  34014  rhmpreimacnlem  34062  rrhre  34199  mbfmcnvima  34433  imambfm  34440  eulerpartgbij  34550  erdszelem1  35407  erdsze  35418  erdsze2lem2  35420  cvmscbv  35474  cvmsi  35481  cvmsval  35482  cvmliftlem15  35514  opelco3  35991  brimageg  36141  fnimage  36143  imageval  36144  fvimage  36145  filnetlem4  36597  bj-imdirval3  37439  bj-imdirco  37445  ptrest  37870  ismtyhmeolem  38055  ismtybndlem  38057  heibor1lem  38060  zndvdchrrhm  42342  aks6d1c7lem2  42551  aks5lem4a  42560  lmhmfgima  43441  brtrclfv2  44083  csbfv12gALTVD  45254  icccncfext  46245  sge0f1o  46740  smfresal  47146  smfpimbor1lem1  47156  smfpimbor1lem2  47157  smfco  47160  f1cof1b  47437  fnfocofob  47439  imaelsetpreimafv  47755  fundcmpsurinjlem3  47760  imasetpreimafvbijlemfo  47765  fundcmpsurbijinjpreimafv  47767  grimco  48249  uhgrimedgi  48250  isuspgrim0  48254  isuspgrimlem  48255  upgrimwlklem5  48261  gricushgr  48277  grimedg  48295  grtrimap  48308  isubgr3stgrlem5  48330  isubgr3stgrlem6  48331  isubgr3stgrlem7  48332  isubgr3stgrlem8  48333  uspgrlimlem4  48351  grlimedgclnbgr  48355  grlimgrtrilem2  48362