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

Theorem funeqi 5428
 Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
funeqi.1
Assertion
Ref Expression
funeqi

Proof of Theorem funeqi
StepHypRef Expression
1 funeqi.1 . 2
2 funeq 5427 . 2
31, 2ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wb 177   wceq 1649   wfun 5402 This theorem is referenced by:  funmpt  5443  funmpt2  5444  funco  5445  funprg  5454  funtpg  5455  funtp  5457  funcnvuni  5472  f1cnvcnv  5601  f1co  5602  fun11iun  5649  f10  5663  funoprabg  6122  mpt2fun  6125  ovidig  6144  tposfun  6445  opabiotafun  6486  tfr1a  6605  tz7.44lem1  6613  tz7.48-2  6649  abianfp  6666  th3qcor  6962  ssdomg  7103  sbthlem7  7173  sbthlem8  7174  1sdom  7261  hartogslem1  7458  r1funlim  7639  zorn2lem4  8326  axaddf  8967  axmulf  8968  structfun  13422  strlemor1  13497  strleun  13500  fthoppc  14061  volf  19364  dfrelog  20402  0trl  21482  0pth  21496  1pthonlem1  21509  2pthonlem1  21519  ajfuni  22281  hlimf  22660  funadj  23309  funcnvadj  23316  rinvf1o  23962  funcnvmptOLD  24002  frrlem10  25475  funpartfun  25665  funtransport  25838  funray  25947  funline  25949  funresfunco  27819  funcoressn  27821  2pthlem1  27976  bnj97  28883  bnj150  28893  bnj1384  29047  bnj1421  29057  bnj60  29077 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-in 3284  df-ss 3291  df-br 4168  df-opab 4222  df-rel 4839  df-cnv 4840  df-co 4841  df-fun 5410
 Copyright terms: Public domain W3C validator