Theorem imaeq2 6030

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 5948	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5905	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5654	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5654	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2790	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  ran crn 5642   ↾ cres 5643   “ cima 5644

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  imaeq2i  6032  imaeq2d  6034  relimasn  6059  cnvimassrndm  6128  funimaexgOLD  6607  fimadmfo  6784  ssimaex  6949  ssimaexg  6950  isoselem  7319  isowe2  7328  f1opw2  7647  mptcnfimad  7968  fnse  8115  supp0cosupp0  8190  tz7.49  8416  ecexr  8679  fopwdom  9054  sbthlem2  9058  sbth  9067  ssenen  9121  sbthfi  9169  fodomfi  9268  imafiOLD  9272  domunfican  9279  fodomfiOLD  9288  f1opwfi  9314  fipreima  9316  marypha1lem  9391  ordtypelem2  9479  ordtypelem3  9480  ordtypelem9  9486  dfac12lem2  10105  dfac12r  10107  ackbij2lem2  10199  ackbij2lem3  10200  r1om  10203  enfin2i  10281  zorn2lem6  10461  zorn2lem7  10462  isacs5lem  18511  acsdrscl  18512  gicsubgen  19218  ghmqusnsglem1  19219  ghmquskerlem1  19222  ghmquskerco  19223  gicqusker  19227  efgrelexlema  19686  tgcn  23146  subbascn  23148  iscnp4  23157  cnpnei  23158  cnima  23159  iscncl  23163  cncls  23168  cnconst2  23177  cnrest2  23180  cnprest  23183  cnindis  23186  cncmp  23286  cmpfi  23302  2ndcomap  23352  ptbasfi  23475  xkoopn  23483  xkoccn  23513  txcnp  23514  ptcnplem  23515  txcnmpt  23518  ptrescn  23533  xkoco1cn  23551  xkoco2cn  23552  xkococn  23554  xkoinjcn  23581  elqtop  23591  qtopomap  23612  qtopcmap  23613  ordthmeolem  23695  fbasrn  23778  elfm  23841  elfm2  23842  elfm3  23844  imaelfm  23845  rnelfmlem  23846  rnelfm  23847  fmfnfmlem2  23849  fmfnfmlem3  23850  fmfnfmlem4  23851  fmco  23855  flffbas  23889  lmflf  23899  fcfneii  23931  ptcmplem3  23948  ptcmplem5  23950  ptcmpg  23951  cnextcn  23961  symgtgp  24000  ghmcnp  24009  eltsms  24027  tsmsf1o  24039  fmucnd  24186  ucnextcn  24198  metcnp3  24435  mbfdm  25534  ismbf  25536  mbfima  25538  ismbfd  25547  mbfimaopnlem  25563  mbfimaopn2  25565  i1fd  25589  ellimc2  25785  limcflf  25789  xrlimcnp  26885  oldval  27769  ubthlem1  30806  disjpreima  32520  imadifxp  32537  preimane  32601  fnpreimac  32602  lmicqusker  33396  ricqusker  33405  algextdeglem4  33717  algextdeg  33722  qtophaus  33833  rhmpreimacnlem  33881  rrhre  34018  mbfmcnvima  34253  imambfm  34260  eulerpartgbij  34370  erdszelem1  35185  erdsze  35196  erdsze2lem2  35198  cvmscbv  35252  cvmsi  35259  cvmsval  35260  cvmliftlem15  35292  opelco3  35769  brimageg  35922  fnimage  35924  imageval  35925  fvimage  35926  filnetlem4  36376  bj-imdirval3  37179  bj-imdirco  37185  ptrest  37620  ismtyhmeolem  37805  ismtybndlem  37807  heibor1lem  37810  zndvdchrrhm  41967  aks6d1c7lem2  42176  aks5lem4a  42185  lmhmfgima  43080  brtrclfv2  43723  csbfv12gALTVD  44895  icccncfext  45892  sge0f1o  46387  smfresal  46793  smfpimbor1lem1  46803  smfpimbor1lem2  46804  smfco  46807  f1cof1b  47082  fnfocofob  47084  imaelsetpreimafv  47400  fundcmpsurinjlem3  47405  imasetpreimafvbijlemfo  47410  fundcmpsurbijinjpreimafv  47412  grimco  47893  uhgrimedgi  47894  isuspgrim0  47898  isuspgrimlem  47899  upgrimwlklem5  47905  gricushgr  47921  grimedg  47939  grtrimap  47951  isubgr3stgrlem5  47973  isubgr3stgrlem6  47974  isubgr3stgrlem7  47975  isubgr3stgrlem8  47976  uspgrlimlem4  47994  grlimgrtrilem2  47998