Theorem imaeq2 6054

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 5975	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5936	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5688	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5688	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2795	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688

This theorem is referenced by:  imaeq2i  6056  imaeq2d  6058  relimasn  6082  cnvimassrndm  6150  funimaexgOLD  6634  fimadmfo  6813  ssimaex  6975  ssimaexg  6976  isoselem  7340  isowe2  7349  f1opw2  7663  fnse  8121  supp0cosupp0  8195  tz7.49  8447  ecexr  8710  fopwdom  9082  sbthlem2  9086  sbth  9095  ssenen  9153  imafi  9177  sbthfi  9204  domunfican  9322  fodomfi  9327  f1opwfi  9358  fipreima  9360  marypha1lem  9430  ordtypelem2  9516  ordtypelem3  9517  ordtypelem9  9523  dfac12lem2  10141  dfac12r  10143  ackbij2lem2  10237  ackbij2lem3  10238  r1om  10241  enfin2i  10318  zorn2lem6  10498  zorn2lem7  10499  isacs5lem  18502  acsdrscl  18503  gicsubgen  19193  efgrelexlema  19658  tgcn  22976  subbascn  22978  iscnp4  22987  cnpnei  22988  cnima  22989  iscncl  22993  cncls  22998  cnconst2  23007  cnrest2  23010  cnprest  23013  cnindis  23016  cncmp  23116  cmpfi  23132  2ndcomap  23182  ptbasfi  23305  xkoopn  23313  xkoccn  23343  txcnp  23344  ptcnplem  23345  txcnmpt  23348  ptrescn  23363  xkoco1cn  23381  xkoco2cn  23382  xkococn  23384  xkoinjcn  23411  elqtop  23421  qtopomap  23442  qtopcmap  23443  ordthmeolem  23525  fbasrn  23608  elfm  23671  elfm2  23672  elfm3  23674  imaelfm  23675  rnelfmlem  23676  rnelfm  23677  fmfnfmlem2  23679  fmfnfmlem3  23680  fmfnfmlem4  23681  fmco  23685  flffbas  23719  lmflf  23729  fcfneii  23761  ptcmplem3  23778  ptcmplem5  23780  ptcmpg  23781  cnextcn  23791  symgtgp  23830  ghmcnp  23839  eltsms  23857  tsmsf1o  23869  fmucnd  24017  ucnextcn  24029  metcnp3  24269  mbfdm  25375  ismbf  25377  mbfima  25379  ismbfd  25388  mbfimaopnlem  25404  mbfimaopn2  25406  i1fd  25430  ellimc2  25626  limcflf  25630  xrlimcnp  26709  oldval  27586  ubthlem1  30390  disjpreima  32082  imadifxp  32099  preimane  32162  fnpreimac  32163  ghmquskerlem1  32802  ghmquskerco  32803  gicqusker  32807  lmicqusker  32809  ricqusker  32819  algextdeglem4  33065  algextdeg  33070  qtophaus  33114  rhmpreimacnlem  33162  rrhre  33299  mbfmcnvima  33552  imambfm  33559  eulerpartgbij  33669  erdszelem1  34480  erdsze  34491  erdsze2lem2  34493  cvmscbv  34547  cvmsi  34554  cvmsval  34555  cvmliftlem15  34587  opelco3  35050  brimageg  35203  fnimage  35205  imageval  35206  fvimage  35207  filnetlem4  35569  bj-imdirval3  36368  bj-imdirco  36374  ptrest  36790  ismtyhmeolem  36975  ismtybndlem  36977  heibor1lem  36980  lmhmfgima  42128  brtrclfv2  42780  csbfv12gALTVD  43962  icccncfext  44901  sge0f1o  45396  smfresal  45802  smfpimbor1lem1  45812  smfpimbor1lem2  45813  smfco  45816  f1cof1b  46083  fnfocofob  46085  imaelsetpreimafv  46361  fundcmpsurinjlem3  46366  imasetpreimafvbijlemfo  46371  fundcmpsurbijinjpreimafv  46373  isomushgr  46792  isomuspgrlem1  46793  isomuspgrlem2a  46794  isomuspgrlem2b  46795  isomuspgrlem2c  46796  isomuspgrlem2d  46797  isomuspgr  46800  isomgrsym  46802