Theorem funeqd 6528

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1550  Fun wfun 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ss 3912  df-br 5091  df-opab 5153  df-rel 5643  df-cnv 5644  df-co 5645  df-fun 6508

This theorem is referenced by:  funopg  6540  funsng  6557  f1eq1  6740  f1ssf1  6824  fvn0ssdmfun  7040  funcnvuni  7898  fundmge2nop0  14501  funcnvs2  14912  funcnvs3  14913  funcnvs4  14914  shftfn  15072  isstruct2  17157  structfung  17162  strle1  17166  setsfun  17179  setsfun0  17180  monfval  17737  ismon  17738  monpropd  17742  isepi  17745  isfth  17921  estrres  18143  lubfun  18354  glbfun  18367  acsficl2d  18556  ebtwntg  29118  ecgrtg  29119  elntg  29120  uhgrspansubgrlem  29426  istrl  29830  ispth  29856  isspth  29857  dfpth2  29864  upgrwlkdvspth  29874  uhgrwkspthlem1  29888  uhgrwkspthlem2  29889  usgr2wlkspthlem1  29892  usgr2wlkspthlem2  29893  pthdlem1  29901  2spthd  30076  0spth  30263  3spthd  30313  trlsegvdeglem2  30358  trlsegvdeglem3  30359  ajfun  30998  fresf1o  32772  padct  32859  smatrcl  34037  esum2dlem  34333  omssubadd  34541  sitgf  34588  funen1cnv  35329  pthhashvtx  35416  satfv0fun  35659  satffunlem1  35695  satffunlem2  35696  satffun  35697  satefvfmla0  35706  satefvfmla1  35713  fperdvper  46431  ovnovollem1  47168  funressnmo  47578  dfateq12d  47658  afvres  47704  funressndmafv2rn  47755  afv2res  47771  upgrimpths  48469  fdivval  49099  idfth  49717  idsubc  49719