Theorem funeqd 6053

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

Step	Hyp	Ref	Expression
1		funeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		funeq 6051	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1631  Fun wfun 6025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-in 3730  df-ss 3737  df-br 4787  df-opab 4847  df-rel 5256  df-cnv 5257  df-co 5258  df-fun 6033

This theorem is referenced by:  funopg  6065  funsng  6080  f1eq1  6236  f1ssf1  6309  fvn0ssdmfun  6493  funcnvuni  7266  fundmge2nop0  13476  funcnvs2  13867  funcnvs3  13868  funcnvs4  13869  shftfn  14021  isstruct2  16074  structfung  16079  setsfun  16100  setsfun0  16101  strle1  16181  monfval  16599  ismon  16600  monpropd  16604  isepi  16607  isfth  16781  estrresOLD  16986  estrres  16987  lubfun  17188  glbfun  17201  acsficl2d  17384  frlmphl  20337  eengbas  26082  ebtwntg  26083  ecgrtg  26084  elntg  26085  uhgrspansubgrlem  26405  istrl  26828  ispth  26854  isspth  26855  upgrwlkdvspth  26870  uhgrwkspthlem1  26884  uhgrwkspthlem2  26885  usgr2wlkspthlem1  26888  usgr2wlkspthlem2  26889  pthdlem1  26897  2spthd  27088  0spth  27306  3spthd  27356  trlsegvdeglem2  27401  trlsegvdeglem3  27402  ajfun  28056  fresf1o  29773  padct  29837  smatrcl  30202  esum2dlem  30494  omssubadd  30702  sitgf  30749  fperdvper  40651  ovnovollem1  41390  dfateq12d  41729  afvres  41772  fdivval  42861