Theorem funeqd 6504

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  Fun wfun 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3920  df-br 5093  df-opab 5155  df-rel 5626  df-cnv 5627  df-co 5628  df-fun 6484

This theorem is referenced by:  funopg  6516  funsng  6533  f1eq1  6715  f1ssf1  6796  fvn0ssdmfun  7008  funcnvuni  7865  fundmge2nop0  14409  funcnvs2  14820  funcnvs3  14821  funcnvs4  14822  shftfn  14980  isstruct2  17060  structfung  17065  strle1  17069  setsfun  17082  setsfun0  17083  monfval  17639  ismon  17640  monpropd  17644  isepi  17647  isfth  17823  estrres  18045  lubfun  18256  glbfun  18269  acsficl2d  18458  ebtwntg  28927  ecgrtg  28928  elntg  28929  uhgrspansubgrlem  29235  istrl  29640  ispth  29666  isspth  29667  dfpth2  29674  upgrwlkdvspth  29684  uhgrwkspthlem1  29698  uhgrwkspthlem2  29699  usgr2wlkspthlem1  29702  usgr2wlkspthlem2  29703  pthdlem1  29711  2spthd  29886  0spth  30070  3spthd  30120  trlsegvdeglem2  30165  trlsegvdeglem3  30166  ajfun  30804  fresf1o  32575  padct  32663  smatrcl  33769  esum2dlem  34065  omssubadd  34274  sitgf  34321  funen1cnv  35061  pthhashvtx  35111  satfv0fun  35354  satffunlem1  35390  satffunlem2  35391  satffun  35392  satefvfmla0  35401  satefvfmla1  35408  fperdvper  45910  ovnovollem1  46647  funressnmo  47040  dfateq12d  47120  afvres  47166  funressndmafv2rn  47217  afv2res  47233  upgrimpths  47903  fdivval  48534  idfth  49153  idsubc  49155