Theorem funeqd 6456

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 6454	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  Fun wfun 6427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-br 5075  df-opab 5137  df-rel 5596  df-cnv 5597  df-co 5598  df-fun 6435

This theorem is referenced by:  funopg  6468  funsng  6485  f1eq1  6665  f1ssf1  6748  fvn0ssdmfun  6952  funcnvuni  7778  fundmge2nop0  14206  funcnvs2  14626  funcnvs3  14627  funcnvs4  14628  shftfn  14784  isstruct2  16850  structfung  16855  strle1  16859  setsfun  16872  setsfun0  16873  monfval  17444  ismon  17445  monpropd  17449  isepi  17452  isfth  17630  estrres  17856  lubfun  18070  glbfun  18083  acsficl2d  18270  frlmphl  20988  ebtwntg  27350  ecgrtg  27351  elntg  27352  uhgrspansubgrlem  27657  istrl  28064  ispth  28091  isspth  28092  upgrwlkdvspth  28107  uhgrwkspthlem1  28121  uhgrwkspthlem2  28122  usgr2wlkspthlem1  28125  usgr2wlkspthlem2  28126  pthdlem1  28134  2spthd  28306  0spth  28490  3spthd  28540  trlsegvdeglem2  28585  trlsegvdeglem3  28586  ajfun  29222  fresf1o  30966  padct  31054  smatrcl  31746  esum2dlem  32060  omssubadd  32267  sitgf  32314  funen1cnv  33060  pthhashvtx  33089  satfv0fun  33333  satffunlem1  33369  satffunlem2  33370  satffun  33371  satefvfmla0  33380  satefvfmla1  33387  prjcrv0  40470  fperdvper  43460  ovnovollem1  44194  funressnmo  44540  dfateq12d  44618  afvres  44664  funressndmafv2rn  44715  afv2res  44731  fdivval  45885