Theorem funeqd 6558

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  Fun wfun 6530

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-rel 5668  df-cnv 5669  df-co 5670  df-fun 6538

This theorem is used by:  funopg  6570  funsng  6587  f1eq1  6769  f1ssf1  6853  fvn0ssdmfun  7069  funcnvuni  7925  fundmge2nop0  14544  funcnvs2  14955  funcnvs3  14956  funcnvs4  14957  shftfn  15115  isstruct2  17213  structfung  17218  strle1  17222  setsfun  17235  setsfun0  17236  monfval  17793  ismon  17794  monpropd  17798  isepi  17801  isfth  17977  estrres  18199  lubfun  18410  glbfun  18423  acsficl2d  18612  ebtwntg  29341  ecgrtg  29342  elntg  29343  uhgrspansubgrlem  29649  istrl  30053  ispth  30079  isspth  30080  dfpth2  30087  upgrwlkdvspth  30097  uhgrwkspthlem1  30111  uhgrwkspthlem2  30112  usgr2wlkspthlem1  30115  usgr2wlkspthlem2  30116  pthdlem1  30124  2spthd  30299  0spth  30486  3spthd  30536  trlsegvdeglem2  30581  trlsegvdeglem3  30582  ajfun  31221  fresf1o  32985  padct  33072  smatrcl  34195  esum2dlem  34491  omssubadd  34699  sitgf  34746  funen1cnv  35486  pthhashvtx  35628  satfv0fun  35871  satffunlem1  35907  satffunlem2  35908  satffun  35909  satefvfmla0  35918  satefvfmla1  35925  fperdvper  46661  ovnovollem1  47398  funressnmo  47811  dfateq12d  47891  afvres  47937  funressndmafv2rn  47988  afv2res  48004  upgrimpths  48702  fdivval  49347  idfth  49964  idsubc  49966