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

Theorem funeqd 5292
Description: Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
Hypothesis
Ref Expression
funeqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
funeqd  |-  ( ph  ->  ( Fun  A  <->  Fun  B ) )

Proof of Theorem funeqd
StepHypRef Expression
1 funeqd.1 . 2  |-  ( ph  ->  A  =  B )
2 funeq 5290 . 2  |-  ( A  =  B  ->  ( Fun  A  <->  Fun  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( Fun  A  <->  Fun  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   Fun wfun 5265
This theorem is referenced by:  funopg  5302  funsng  5314  funcnvuni  5333  f1eq1  5448  shftfn  11584  isstruct2  13173  strle1  13255  monfval  13651  ismon  13652  monpropd  13656  isepi  13659  isfth  13804  acsficl2d  14295  ajfun  21455  cmpmorfun  26074  dfateq12d  28097  afvres  28140  istrl  28336  ispth  28354  isspth  28355  0spth  28357  constr3pthlem2  28402
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