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

Theorem funeqi 5291
Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
funeqi.1  |-  A  =  B
Assertion
Ref Expression
funeqi  |-  ( Fun 
A  <->  Fun  B )

Proof of Theorem funeqi
StepHypRef Expression
1 funeqi.1 . 2  |-  A  =  B
2 funeq 5290 . 2  |-  ( A  =  B  ->  ( Fun  A  <->  Fun  B ) )
31, 2ax-mp 8 1  |-  ( Fun 
A  <->  Fun  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632   Fun wfun 5265
This theorem is referenced by:  funmpt  5306  funmpt2  5307  funco  5308  funprg  5317  funtp  5319  funcnvuni  5333  f1cnvcnv  5461  f1co  5462  fun11iun  5509  f10  5523  funoprabg  5959  mpt2fun  5962  ovidig  5981  tposfun  6266  opabiotafun  6307  tfr1a  6426  tz7.44lem1  6434  tz7.48-2  6470  abianfp  6487  th3qcor  6782  ssdomg  6923  sbthlem7  6993  sbthlem8  6994  1sdom  7081  hartogslem1  7273  r1funlim  7454  zorn2lem4  8142  axaddf  8783  axmulf  8784  structfun  13176  strlemor1  13251  strleun  13254  fthoppc  13813  volf  18904  dfrelog  19939  ajfuni  21454  hlimf  21833  funadj  22482  funcnvadj  22489  rinvf1o  23054  xppreima2  23227  funcnvmptOLD  23249  funcnvmpt  23250  brsiga  23529  frrlem10  24363  funpartfun  24553  funtransport  24726  funray  24835  funline  24837  funresfunco  28093  funcoressn  28095  0trl  28344  0pth  28356  bnj97  29214  bnj150  29224  bnj1384  29378  bnj1421  29388  bnj60  29408
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179  df-br 4040  df-opab 4094  df-rel 4712  df-cnv 4713  df-co 4714  df-fun 5273
  Copyright terms: Public domain W3C validator