Theorem funeqd 6522

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

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

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 3928  df-br 5103  df-opab 5165  df-rel 5638  df-cnv 5639  df-co 5640  df-fun 6501

This theorem is referenced by:  funopg  6534  funsng  6551  f1eq1  6733  f1ssf1  6814  fvn0ssdmfun  7028  funcnvuni  7888  fundmge2nop0  14443  funcnvs2  14855  funcnvs3  14856  funcnvs4  14857  shftfn  15015  isstruct2  17095  structfung  17100  strle1  17104  setsfun  17117  setsfun0  17118  monfval  17674  ismon  17675  monpropd  17679  isepi  17682  isfth  17858  estrres  18080  lubfun  18291  glbfun  18304  acsficl2d  18493  ebtwntg  28962  ecgrtg  28963  elntg  28964  uhgrspansubgrlem  29270  istrl  29675  ispth  29701  isspth  29702  dfpth2  29709  upgrwlkdvspth  29719  uhgrwkspthlem1  29733  uhgrwkspthlem2  29734  usgr2wlkspthlem1  29737  usgr2wlkspthlem2  29738  pthdlem1  29746  2spthd  29921  0spth  30105  3spthd  30155  trlsegvdeglem2  30200  trlsegvdeglem3  30201  ajfun  30839  fresf1o  32605  padct  32693  smatrcl  33779  esum2dlem  34075  omssubadd  34284  sitgf  34331  funen1cnv  35071  pthhashvtx  35108  satfv0fun  35351  satffunlem1  35387  satffunlem2  35388  satffun  35389  satefvfmla0  35398  satefvfmla1  35405  fperdvper  45910  ovnovollem1  46647  funressnmo  47040  dfateq12d  47120  afvres  47166  funressndmafv2rn  47217  afv2res  47233  upgrimpths  47902  fdivval  48521  idfth  49140  idsubc  49142