Theorem funeqd 6589

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  Fun wfun 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-br 5148  df-opab 5210  df-rel 5695  df-cnv 5696  df-co 5697  df-fun 6564

This theorem is referenced by:  funopg  6601  funsng  6618  f1eq1  6799  f1ssf1  6880  fvn0ssdmfun  7093  funcnvuni  7954  fundmge2nop0  14537  funcnvs2  14948  funcnvs3  14949  funcnvs4  14950  shftfn  15108  isstruct2  17182  structfung  17187  strle1  17191  setsfun  17204  setsfun0  17205  monfval  17779  ismon  17780  monpropd  17784  isepi  17787  isfth  17967  estrres  18194  lubfun  18409  glbfun  18422  acsficl2d  18609  ebtwntg  29011  ecgrtg  29012  elntg  29013  uhgrspansubgrlem  29321  istrl  29728  ispth  29755  isspth  29756  upgrwlkdvspth  29771  uhgrwkspthlem1  29785  uhgrwkspthlem2  29786  usgr2wlkspthlem1  29789  usgr2wlkspthlem2  29790  pthdlem1  29798  2spthd  29970  0spth  30154  3spthd  30204  trlsegvdeglem2  30249  trlsegvdeglem3  30250  ajfun  30888  fresf1o  32647  padct  32736  smatrcl  33756  esum2dlem  34072  omssubadd  34281  sitgf  34328  funen1cnv  35080  pthhashvtx  35111  satfv0fun  35355  satffunlem1  35391  satffunlem2  35392  satffun  35393  satefvfmla0  35402  satefvfmla1  35409  fperdvper  45874  ovnovollem1  46611  funressnmo  46995  dfateq12d  47075  afvres  47121  funressndmafv2rn  47172  afv2res  47188  fdivval  48388