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

Theorem funeqd 5874
Description: Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
Hypothesis
Ref Expression
funeqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
funeqd (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))

Proof of Theorem funeqd
StepHypRef Expression
1 funeqd.1 . 2 (𝜑𝐴 = 𝐵)
2 funeq 5872 . 2 (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
31, 2syl 17 1 (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  Fun wfun 5846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-in 3566  df-ss 3573  df-br 4619  df-opab 4679  df-rel 5086  df-cnv 5087  df-co 5088  df-fun 5854
This theorem is referenced by:  funopg  5885  funsng  5900  f1eq1  6058  f1ssf1  6130  fvn0ssdmfun  6311  funcnvuni  7073  fundmge2nop0  13221  funcnvs2  13602  funcnvs3  13603  funcnvs4  13604  shftfn  13755  isstruct2  15801  structfung  15806  setsfun  15825  setsfun0  15826  strle1  15905  monfval  16324  ismon  16325  monpropd  16329  isepi  16332  isfth  16506  estrres  16711  lubfun  16912  glbfun  16925  acsficl2d  17108  frlmphl  20052  eengbas  25778  ebtwntg  25779  ecgrtg  25780  elntg  25781  uhgrspansubgrlem  26092  istrl  26479  ispth  26505  isspth  26506  upgrwlkdvspth  26521  uhgrwkspthlem1  26535  uhgrwkspthlem2  26536  usgr2wlkspthlem1  26539  usgr2wlkspthlem2  26540  pthdlem1  26548  2spthd  26723  0spth  26870  3spthd  26919  trlsegvdeglem2  26964  trlsegvdeglem3  26965  ajfun  27586  fresf1o  29300  padct  29363  smatrcl  29668  esum2dlem  29959  omssubadd  30167  sitgf  30214  fperdvper  39466  ovnovollem1  40203  dfateq12d  40539  afvres  40582  fdivval  41651
  Copyright terms: Public domain W3C validator