Theorem funeqd 6580

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  Fun wfun 6547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ss 3963  df-br 5153  df-opab 5215  df-rel 5688  df-cnv 5689  df-co 5690  df-fun 6555

This theorem is referenced by:  funopg  6592  funsng  6609  f1eq1  6792  f1ssf1  6874  fvn0ssdmfun  7087  funcnvuni  7944  fundmge2nop0  14506  funcnvs2  14917  funcnvs3  14918  funcnvs4  14919  shftfn  15073  isstruct2  17146  structfung  17151  strle1  17155  setsfun  17168  setsfun0  17169  monfval  17743  ismon  17744  monpropd  17748  isepi  17751  isfth  17931  estrres  18158  lubfun  18372  glbfun  18385  acsficl2d  18572  ebtwntg  28908  ecgrtg  28909  elntg  28910  uhgrspansubgrlem  29218  istrl  29625  ispth  29652  isspth  29653  upgrwlkdvspth  29668  uhgrwkspthlem1  29682  uhgrwkspthlem2  29683  usgr2wlkspthlem1  29686  usgr2wlkspthlem2  29687  pthdlem1  29695  2spthd  29867  0spth  30051  3spthd  30101  trlsegvdeglem2  30146  trlsegvdeglem3  30147  ajfun  30785  fresf1o  32539  padct  32624  smatrcl  33567  esum2dlem  33881  omssubadd  34090  sitgf  34137  funen1cnv  34881  pthhashvtx  34907  satfv0fun  35151  satffunlem1  35187  satffunlem2  35188  satffun  35189  satefvfmla0  35198  satefvfmla1  35205  fperdvper  45477  ovnovollem1  46214  funressnmo  46598  dfateq12d  46676  afvres  46722  funressndmafv2rn  46773  afv2res  46789  fdivval  47864