Theorem funeqd 6511

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  Fun wfun 6483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ss 3902  df-br 5076  df-opab 5138  df-rel 5628  df-cnv 5629  df-co 5630  df-fun 6491

This theorem is referenced by:  funopg  6523  funsng  6540  f1eq1  6722  f1ssf1  6803  fvn0ssdmfun  7019  funcnvuni  7876  fundmge2nop0  14459  funcnvs2  14870  funcnvs3  14871  funcnvs4  14872  shftfn  15030  isstruct2  17114  structfung  17119  strle1  17123  setsfun  17136  setsfun0  17137  monfval  17694  ismon  17695  monpropd  17699  isepi  17702  isfth  17878  estrres  18100  lubfun  18311  glbfun  18324  acsficl2d  18513  ebtwntg  29073  ecgrtg  29074  elntg  29075  uhgrspansubgrlem  29381  istrl  29785  ispth  29811  isspth  29812  dfpth2  29819  upgrwlkdvspth  29829  uhgrwkspthlem1  29843  uhgrwkspthlem2  29844  usgr2wlkspthlem1  29847  usgr2wlkspthlem2  29848  pthdlem1  29856  2spthd  30031  0spth  30218  3spthd  30268  trlsegvdeglem2  30313  trlsegvdeglem3  30314  ajfun  30953  fresf1o  32727  padct  32814  smatrcl  33992  esum2dlem  34288  omssubadd  34496  sitgf  34543  funen1cnv  35284  pthhashvtx  35371  satfv0fun  35614  satffunlem1  35650  satffunlem2  35651  satffun  35652  satefvfmla0  35661  satefvfmla1  35668  fperdvper  46376  ovnovollem1  47113  funressnmo  47523  dfateq12d  47603  afvres  47649  funressndmafv2rn  47700  afv2res  47716  upgrimpths  48414  fdivval  49044  idfth  49662  idsubc  49664