Theorem funeqd 6071

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632  Fun wfun 6043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-in 3722  df-ss 3729  df-br 4805  df-opab 4865  df-rel 5273  df-cnv 5274  df-co 5275  df-fun 6051

This theorem is referenced by:  funopg  6083  funsng  6098  f1eq1  6257  f1ssf1  6329  fvn0ssdmfun  6513  funcnvuni  7284  fundmge2nop0  13466  funcnvs2  13858  funcnvs3  13859  funcnvs4  13860  shftfn  14012  isstruct2  16069  structfung  16074  setsfun  16095  setsfun0  16096  strle1  16175  monfval  16593  ismon  16594  monpropd  16598  isepi  16601  isfth  16775  estrres  16980  lubfun  17181  glbfun  17194  acsficl2d  17377  frlmphl  20322  eengbas  26060  ebtwntg  26061  ecgrtg  26062  elntg  26063  uhgrspansubgrlem  26381  istrl  26803  ispth  26829  isspth  26830  upgrwlkdvspth  26845  uhgrwkspthlem1  26859  uhgrwkspthlem2  26860  usgr2wlkspthlem1  26863  usgr2wlkspthlem2  26864  pthdlem1  26872  2spthd  27061  0spth  27278  3spthd  27328  trlsegvdeglem2  27373  trlsegvdeglem3  27374  ajfun  28025  fresf1o  29742  padct  29806  smatrcl  30171  esum2dlem  30463  omssubadd  30671  sitgf  30718  fperdvper  40636  ovnovollem1  41376  dfateq12d  41715  afvres  41758  fdivval  42843