Theorem imaeq2 6060

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 5930	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5676	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5676	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2825	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5664   ↾ cres 5665   “ cima 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is used by:  imaeq2i  6062  imaeq2d  6064  relimasn  6089  cnvimassrndm  6151  fimadmfo  6805  ssimaex  6970  ssimaexg  6971  isoselem  7348  isowe2  7357  f1opw2  7675  mptcnfimad  7989  fnse  8135  supp0cosupp0  8210  tz7.49  8438  ecexr  8705  fopwdom  9080  sbthlem2  9083  sbth  9092  ssenen  9146  sbthfi  9190  fodomfi  9279  domunfican  9288  f1opwfi  9320  fipreima  9322  marypha1lem  9400  ordtypelem2  9488  ordtypelem3  9489  ordtypelem9  9495  dfac12lem2  10144  dfac12r  10146  ackbij2lem2  10238  ackbij2lem3  10239  r1om  10242  enfin2i  10320  zorn2lem6  10500  zorn2lem7  10501  isacs5lem  18623  acsdrscl  18624  gicsubgen  19393  ghmqusnsglem1  19394  ghmquskerlem1  19397  ghmquskerco  19398  gicqusker  19402  efgrelexlema  19863  tgcn  23459  subbascn  23461  iscnp4  23470  cnpnei  23471  cnima  23472  iscncl  23476  cncls  23481  cnconst2  23490  cnrest2  23493  cnprest  23496  cnindis  23499  cncmp  23599  cmpfi  23615  2ndcomap  23666  ptbasfi  23789  xkoopn  23797  xkoccn  23827  txcnp  23828  ptcnplem  23829  txcnmpt  23832  ptrescn  23847  xkoco1cn  23865  xkoco2cn  23866  xkococn  23868  xkoinjcn  23895  elqtop  23905  qtopomap  23926  qtopcmap  23927  ordthmeolem  24009  fbasrn  24092  elfm  24155  elfm2  24156  elfm3  24158  imaelfm  24159  rnelfmlem  24160  rnelfm  24161  fmfnfmlem2  24163  fmfnfmlem3  24164  fmfnfmlem4  24165  fmco  24169  flffbas  24203  lmflf  24213  fcfneii  24245  ptcmplem3  24262  ptcmplem5  24264  ptcmpg  24265  cnextcn  24275  symgtgp  24314  ghmcnp  24323  eltsms  24341  tsmsf1o  24353  fmucnd  24499  ucnextcn  24511  metcnp3  24748  mbfdm  25836  ismbf  25838  mbfima  25840  ismbfd  25849  mbfimaopnlem  25865  mbfimaopn2  25867  i1fd  25891  ellimc2  26087  limcflf  26091  xrlimcnp  27184  oldval  28078  ubthlem1  31293  disjpreima  33000  imadifxp  33017  preimane  33085  fnpreimac  33086  lmicqusker  33791  ricqusker  33799  algextdeglem4  34174  algextdeg  34179  qtophaus  34290  rhmpreimacnlem  34338  rrhre  34475  mbfmcnvima  34710  imambfm  34717  eulerpartgbij  34827  erdszelem1  35720  erdsze  35731  erdsze2lem2  35733  cvmscbv  35787  cvmsi  35794  cvmsval  35795  cvmliftlem15  35827  opelco3  36304  brimageg  36454  fnimage  36456  imageval  36457  fvimage  36458  filnetlem4  36949  bj-imdirval3  37885  bj-imdirco  37891  ptrest  38327  ismtyhmeolem  38513  ismtybndlem  38515  heibor1lem  38518  zndvdchrrhm  42798  aks6d1c7lem2  43006  aks5lem4a  43015  lmhmfgima  43869  brtrclfv2  44511  csbfv12gALTVD  45665  icccncfext  46659  sge0f1o  47154  smfresal  47560  smfpimbor1lem1  47570  smfpimbor1lem2  47571  smfco  47574  f1cof1b  47872  fnfocofob  47874  imaelsetpreimafv  48202  fundcmpsurinjlem3  48207  imasetpreimafvbijlemfo  48212  fundcmpsurbijinjpreimafv  48214  grimco  48712  uhgrimedgi  48713  isuspgrim0  48717  isuspgrimlem  48718  upgrimwlklem5  48724  gricushgr  48740  grimedg  48758  grtrimap  48771  isubgr3stgrlem5  48793  isubgr3stgrlem6  48794  isubgr3stgrlem7  48795  isubgr3stgrlem8  48796  uspgrlimlem4  48814  grlimedgclnbgr  48818  grlimgrtrilem2  48825