Theorem funeqd 6570

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  Fun wfun 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-br 5149  df-opab 5211  df-rel 5683  df-cnv 5684  df-co 5685  df-fun 6545

This theorem is referenced by:  funopg  6582  funsng  6599  f1eq1  6782  f1ssf1  6865  fvn0ssdmfun  7076  funcnvuni  7924  fundmge2nop0  14457  funcnvs2  14868  funcnvs3  14869  funcnvs4  14870  shftfn  15024  isstruct2  17086  structfung  17091  strle1  17095  setsfun  17108  setsfun0  17109  monfval  17683  ismon  17684  monpropd  17688  isepi  17691  isfth  17869  estrres  18095  lubfun  18309  glbfun  18322  acsficl2d  18509  ebtwntg  28495  ecgrtg  28496  elntg  28497  uhgrspansubgrlem  28802  istrl  29208  ispth  29235  isspth  29236  upgrwlkdvspth  29251  uhgrwkspthlem1  29265  uhgrwkspthlem2  29266  usgr2wlkspthlem1  29269  usgr2wlkspthlem2  29270  pthdlem1  29278  2spthd  29450  0spth  29634  3spthd  29684  trlsegvdeglem2  29729  trlsegvdeglem3  29730  ajfun  30368  fresf1o  32110  padct  32199  smatrcl  33062  esum2dlem  33376  omssubadd  33585  sitgf  33632  funen1cnv  34377  pthhashvtx  34404  satfv0fun  34648  satffunlem1  34684  satffunlem2  34685  satffun  34686  satefvfmla0  34695  satefvfmla1  34702  fperdvper  44934  ovnovollem1  45671  funressnmo  46055  dfateq12d  46133  afvres  46179  funressndmafv2rn  46230  afv2res  46246  fdivval  47313