Theorem funeqd 6538

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

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

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 3931  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-fun 6513

This theorem is referenced by:  funopg  6550  funsng  6567  f1eq1  6751  f1ssf1  6832  fvn0ssdmfun  7046  funcnvuni  7908  fundmge2nop0  14467  funcnvs2  14879  funcnvs3  14880  funcnvs4  14881  shftfn  15039  isstruct2  17119  structfung  17124  strle1  17128  setsfun  17141  setsfun0  17142  monfval  17694  ismon  17695  monpropd  17699  isepi  17702  isfth  17878  estrres  18100  lubfun  18311  glbfun  18324  acsficl2d  18511  ebtwntg  28909  ecgrtg  28910  elntg  28911  uhgrspansubgrlem  29217  istrl  29624  ispth  29651  isspth  29652  dfpth2  29659  upgrwlkdvspth  29669  uhgrwkspthlem1  29683  uhgrwkspthlem2  29684  usgr2wlkspthlem1  29687  usgr2wlkspthlem2  29688  pthdlem1  29696  2spthd  29871  0spth  30055  3spthd  30105  trlsegvdeglem2  30150  trlsegvdeglem3  30151  ajfun  30789  fresf1o  32555  padct  32643  smatrcl  33786  esum2dlem  34082  omssubadd  34291  sitgf  34338  funen1cnv  35078  pthhashvtx  35115  satfv0fun  35358  satffunlem1  35394  satffunlem2  35395  satffun  35396  satefvfmla0  35405  satefvfmla1  35412  fperdvper  45917  ovnovollem1  46654  funressnmo  47047  dfateq12d  47127  afvres  47173  funressndmafv2rn  47224  afv2res  47240  upgrimpths  47909  fdivval  48528  idfth  49147  idsubc  49149