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

Theorem funeqi 5275
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 5274 . 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 1623   Fun wfun 5249
This theorem is referenced by:  funmpt  5290  funmpt2  5291  funco  5292  funprg  5301  funtp  5303  funcnvuni  5317  f1cnvcnv  5445  f1co  5446  fun11iun  5493  f10  5507  funoprabg  5943  mpt2fun  5946  ovidig  5965  tposfun  6250  opabiotafun  6291  tfr1a  6410  tz7.44lem1  6418  tz7.48-2  6454  abianfp  6471  th3qcor  6766  ssdomg  6907  sbthlem7  6977  sbthlem8  6978  1sdom  7065  hartogslem1  7257  r1funlim  7438  zorn2lem4  8126  axaddf  8767  axmulf  8768  structfun  13160  strlemor1  13235  strleun  13238  fthoppc  13797  volf  18888  dfrelog  19923  ajfuni  21438  hlimf  21817  funadj  22466  funcnvadj  22473  rinvf1o  23038  xppreima2  23212  funcnvmptOLD  23234  funcnvmpt  23235  brsiga  23514  frrlem10  24292  funpartfun  24481  funtransport  24654  funray  24763  funline  24765  funresfunco  27988  funcoressn  27990  bnj97  28898  bnj150  28908  bnj1384  29062  bnj1421  29072  bnj60  29092
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-rel 4696  df-cnv 4697  df-co 4698  df-fun 5257
  Copyright terms: Public domain W3C validator