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

Theorem funeqd 5438
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 5436 . 2  |-  ( A  =  B  ->  ( Fun  A  <->  Fun  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( Fun  A  <->  Fun  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   Fun wfun 5411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-in 3334  df-ss 3341  df-br 4292  df-opab 4350  df-rel 4846  df-cnv 4847  df-co 4848  df-fun 5419
This theorem is referenced by:  funopg  5449  funsng  5463  f1eq1  5600  funcnvuni  6529  shftfn  12561  isstruct2  14182  strle1  14268  monfval  14670  ismon  14671  monpropd  14675  isepi  14678  isfth  14823  lubfun  15149  glbfun  15162  acsficl2d  15345  frlmphl  18205  eengbas  23226  ebtwntg  23227  ecgrtg  23228  elntg  23229  istrl  23435  ispth  23466  isspth  23467  0spth  23469  1pthonlem1  23487  constr2spthlem1  23492  2pthlem1  23493  constr2pth  23499  constr3pthlem2  23541  ajfun  24260  sitgf  26732  dfateq12d  30033  afvres  30076  usgra2pthspth  30293
  Copyright terms: Public domain W3C validator