MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq1i Unicode version

Theorem feq1i 5728
Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq1i.1
Assertion
Ref Expression
feq1i

Proof of Theorem feq1i
StepHypRef Expression
1 feq1i.1 . 2
2 feq1 5718 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  -->wf 5589
This theorem is referenced by:  ftpg  6081  suppsnop  6932  seqomlem2  7135  addnqf  9347  mulnqf  9348  hashf  12412  isumsup2  13658  ruclem6  13968  sadcf  14103  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  smupf  14128  algrf  14202  funcoppc  15244  pmtr3ncomlem1  16498  znf1o  18590  ovolfsf  21883  ovolsf  21884  ovoliunlem1  21913  ovoliun  21916  ovoliun2  21917  voliunlem3  21962  itgss3  22221  dvexp  22356  efcn  22838  basellem9  23362  axlowdimlem10  24254  uhgrares  24308  umgrares  24324  2trllemH  24554  2trllemG  24560  wlkntrllem1  24561  wlkntrllem3  24563  eupares  24975  issubgoi  25312  vsfval  25528  ho0f  26670  opsqrlem4  27062  pjinvari  27110  fmptdF  27495  sitgclg  28284  coinfliprv  28421  plymul02  28503  signshf  28545  gamf  28585  circum  29040  diophren  30747  seff  31189  binomcxplemnotnn0  31261  fourierdlem62  31951  fourierdlem80  31969  fourierdlem97  31986  uhgres  32379  mapprop  32935  lindslinindimp2lem2  33060  zlmodzxzldeplem1  33101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-fun 5595  df-fn 5596  df-f 5597
  Copyright terms: Public domain W3C validator