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

Theorem feq2i 5729
Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011.)
Hypothesis
Ref Expression
feq2i.1
Assertion
Ref Expression
feq2i

Proof of Theorem feq2i
StepHypRef Expression
1 feq2i.1 . 2
2 feq2 5719 . 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:  fresaun  5761  fmpt2x  6866  fmpt2  6867  tposf  7002  issmo  7038  axdc3lem4  8854  cardf  8946  smobeth  8982  1fv  11821  seqf2  12126  hashf  12412  wrd0  12565  iswrddm0  12567  wrd2pr2op  12885  ntrivcvgtail  13709  vdwlem8  14506  0ram  14538  gsumws1  16007  ga0  16336  efgsp1  16755  efgsfo  16757  efgredleme  16761  efgred  16766  ablfaclem2  17137  islinds2  18848  pmatcollpw3fi1lem1  19287  0met  20869  dvef  22381  dvfsumrlim2  22433  dchrisum0  23705  trgcgrg  23906  axlowdimlem4  24248  uhgra0  24309  umgra0  24325  0wlk  24547  0trl  24548  wlkntrl  24564  0spth  24573  constr1trl  24590  constr2wlk  24600  constr2trl  24601  usgra2wlkspthlem2  24620  constr3trllem3  24652  constr3trllem4  24653  grposn  25217  mbfmcnt  28239  coinfliprv  28421  fdc  30238  rabren3dioph  30749  fourierdlem80  31969  2ffzoeq  32341  uhg0e  32376
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-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fn 5596  df-f 5597
  Copyright terms: Public domain W3C validator