Theorem funeqd 6512

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  Fun wfun 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916  df-br 5097  df-opab 5159  df-rel 5629  df-cnv 5630  df-co 5631  df-fun 6492

This theorem is referenced by:  funopg  6524  funsng  6541  f1eq1  6723  f1ssf1  6804  fvn0ssdmfun  7017  funcnvuni  7872  fundmge2nop0  14423  funcnvs2  14834  funcnvs3  14835  funcnvs4  14836  shftfn  14994  isstruct2  17074  structfung  17079  strle1  17083  setsfun  17096  setsfun0  17097  monfval  17654  ismon  17655  monpropd  17659  isepi  17662  isfth  17838  estrres  18060  lubfun  18271  glbfun  18284  acsficl2d  18473  ebtwntg  29004  ecgrtg  29005  elntg  29006  uhgrspansubgrlem  29312  istrl  29717  ispth  29743  isspth  29744  dfpth2  29751  upgrwlkdvspth  29761  uhgrwkspthlem1  29775  uhgrwkspthlem2  29776  usgr2wlkspthlem1  29779  usgr2wlkspthlem2  29780  pthdlem1  29788  2spthd  29963  0spth  30150  3spthd  30200  trlsegvdeglem2  30245  trlsegvdeglem3  30246  ajfun  30884  fresf1o  32658  padct  32746  smatrcl  33902  esum2dlem  34198  omssubadd  34406  sitgf  34453  funen1cnv  35193  pthhashvtx  35271  satfv0fun  35514  satffunlem1  35550  satffunlem2  35551  satffun  35552  satefvfmla0  35561  satefvfmla1  35568  fperdvper  46105  ovnovollem1  46842  funressnmo  47234  dfateq12d  47314  afvres  47360  funressndmafv2rn  47411  afv2res  47427  upgrimpths  48097  fdivval  48727  idfth  49345  idsubc  49347