Theorem funeqd 5825

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  Fun wfun 5798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-fun 5806

This theorem is referenced by:  funopg  5836  funsng  5851  f1eq1  6009  fvn0ssdmfun  6258  funcnvuni  7012  fundmge2nop0  13129  funcnvs2  13508  funcnvs3  13509  funcnvs4  13510  shftfn  13661  isstruct2  15704  setsfun  15725  setsfun0  15726  strle1  15800  monfval  16215  ismon  16216  monpropd  16220  isepi  16223  isfth  16397  estrres  16602  lubfun  16803  glbfun  16816  acsficl2d  16999  frlmphl  19939  eengbas  25661  ebtwntg  25662  ecgrtg  25663  elntg  25664  istrl  26067  ispth  26098  isspth  26099  0spth  26101  1pthonlem1  26119  constr2spthlem1  26124  2pthlem1  26125  constr2pth  26131  constr3pthlem2  26184  ajfun  27100  fresf1o  28815  padct  28885  smatrcl  29190  esum2dlem  29481  omssubadd  29689  sitgf  29736  fperdvper  38808  ovnovollem1  39546  dfateq12d  39858  afvres  39901  f1ssf1  40328  uhgrspansubgrlem  40514  isTrl  40904  isPth  40929  issPth  40930  upgrwlkdvspth  40945  uhgr1wlkspthlem1  40959  uhgr1wlkspthlem2  40960  usgr2wlkspthlem1  40963  usgr2wlkspthlem2  40964  pthdlem1  40972  2spthd  41148  0spth-av  41294  3spthd  41343  trlsegvdeglem2  41389  trlsegvdeglem3  41390  fdivval  42131