Theorem funeqd 6567

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  Fun wfun 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-br 5148  df-opab 5210  df-rel 5682  df-cnv 5683  df-co 5684  df-fun 6542

This theorem is referenced by:  funopg  6579  funsng  6596  f1eq1  6779  f1ssf1  6862  fvn0ssdmfun  7073  funcnvuni  7918  fundmge2nop0  14449  funcnvs2  14860  funcnvs3  14861  funcnvs4  14862  shftfn  15016  isstruct2  17078  structfung  17083  strle1  17087  setsfun  17100  setsfun0  17101  monfval  17675  ismon  17676  monpropd  17680  isepi  17683  isfth  17861  estrres  18087  lubfun  18301  glbfun  18314  acsficl2d  18501  ebtwntg  28229  ecgrtg  28230  elntg  28231  uhgrspansubgrlem  28536  istrl  28942  ispth  28969  isspth  28970  upgrwlkdvspth  28985  uhgrwkspthlem1  28999  uhgrwkspthlem2  29000  usgr2wlkspthlem1  29003  usgr2wlkspthlem2  29004  pthdlem1  29012  2spthd  29184  0spth  29368  3spthd  29418  trlsegvdeglem2  29463  trlsegvdeglem3  29464  ajfun  30100  fresf1o  31842  padct  31931  smatrcl  32764  esum2dlem  33078  omssubadd  33287  sitgf  33334  funen1cnv  34079  pthhashvtx  34106  satfv0fun  34350  satffunlem1  34386  satffunlem2  34387  satffun  34388  satefvfmla0  34397  satefvfmla1  34404  fperdvper  44621  ovnovollem1  45358  funressnmo  45742  dfateq12d  45820  afvres  45866  funressndmafv2rn  45917  afv2res  45933  fdivval  47178