Theorem funeqd 6600

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  Fun wfun 6567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-rel 5707  df-cnv 5708  df-co 5709  df-fun 6575

This theorem is referenced by:  funopg  6612  funsng  6629  f1eq1  6812  f1ssf1  6894  fvn0ssdmfun  7108  funcnvuni  7972  fundmge2nop0  14551  funcnvs2  14962  funcnvs3  14963  funcnvs4  14964  shftfn  15122  isstruct2  17196  structfung  17201  strle1  17205  setsfun  17218  setsfun0  17219  monfval  17793  ismon  17794  monpropd  17798  isepi  17801  isfth  17981  estrres  18208  lubfun  18422  glbfun  18435  acsficl2d  18622  ebtwntg  29015  ecgrtg  29016  elntg  29017  uhgrspansubgrlem  29325  istrl  29732  ispth  29759  isspth  29760  upgrwlkdvspth  29775  uhgrwkspthlem1  29789  uhgrwkspthlem2  29790  usgr2wlkspthlem1  29793  usgr2wlkspthlem2  29794  pthdlem1  29802  2spthd  29974  0spth  30158  3spthd  30208  trlsegvdeglem2  30253  trlsegvdeglem3  30254  ajfun  30892  fresf1o  32650  padct  32733  smatrcl  33742  esum2dlem  34056  omssubadd  34265  sitgf  34312  funen1cnv  35064  pthhashvtx  35095  satfv0fun  35339  satffunlem1  35375  satffunlem2  35376  satffun  35377  satefvfmla0  35386  satefvfmla1  35393  fperdvper  45840  ovnovollem1  46577  funressnmo  46961  dfateq12d  47041  afvres  47087  funressndmafv2rn  47138  afv2res  47154  fdivval  48273