Theorem funeqd 6440

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-rel 5587  df-cnv 5588  df-co 5589  df-fun 6420

This theorem is referenced by:  funopg  6452  funsng  6469  f1eq1  6649  f1ssf1  6731  fvn0ssdmfun  6934  funcnvuni  7752  fundmge2nop0  14134  funcnvs2  14554  funcnvs3  14555  funcnvs4  14556  shftfn  14712  isstruct2  16778  structfung  16783  strle1  16787  setsfun  16800  setsfun0  16801  monfval  17361  ismon  17362  monpropd  17366  isepi  17369  isfth  17546  estrres  17772  lubfun  17985  glbfun  17998  acsficl2d  18185  frlmphl  20898  ebtwntg  27253  ecgrtg  27254  elntg  27255  uhgrspansubgrlem  27560  istrl  27966  ispth  27992  isspth  27993  upgrwlkdvspth  28008  uhgrwkspthlem1  28022  uhgrwkspthlem2  28023  usgr2wlkspthlem1  28026  usgr2wlkspthlem2  28027  pthdlem1  28035  2spthd  28207  0spth  28391  3spthd  28441  trlsegvdeglem2  28486  trlsegvdeglem3  28487  ajfun  29123  fresf1o  30867  padct  30956  smatrcl  31648  esum2dlem  31960  omssubadd  32167  sitgf  32214  funen1cnv  32960  pthhashvtx  32989  satfv0fun  33233  satffunlem1  33269  satffunlem2  33270  satffun  33271  satefvfmla0  33280  satefvfmla1  33287  fperdvper  43350  ovnovollem1  44084  funressnmo  44427  dfateq12d  44505  afvres  44551  funressndmafv2rn  44602  afv2res  44618  fdivval  45773