Theorem funeqd 6541

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  Fun wfun 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-fun 6516

This theorem is referenced by:  funopg  6553  funsng  6570  f1eq1  6754  f1ssf1  6835  fvn0ssdmfun  7049  funcnvuni  7911  fundmge2nop0  14474  funcnvs2  14886  funcnvs3  14887  funcnvs4  14888  shftfn  15046  isstruct2  17126  structfung  17131  strle1  17135  setsfun  17148  setsfun0  17149  monfval  17701  ismon  17702  monpropd  17706  isepi  17709  isfth  17885  estrres  18107  lubfun  18318  glbfun  18331  acsficl2d  18518  ebtwntg  28916  ecgrtg  28917  elntg  28918  uhgrspansubgrlem  29224  istrl  29631  ispth  29658  isspth  29659  dfpth2  29666  upgrwlkdvspth  29676  uhgrwkspthlem1  29690  uhgrwkspthlem2  29691  usgr2wlkspthlem1  29694  usgr2wlkspthlem2  29695  pthdlem1  29703  2spthd  29878  0spth  30062  3spthd  30112  trlsegvdeglem2  30157  trlsegvdeglem3  30158  ajfun  30796  fresf1o  32562  padct  32650  smatrcl  33793  esum2dlem  34089  omssubadd  34298  sitgf  34345  funen1cnv  35085  pthhashvtx  35122  satfv0fun  35365  satffunlem1  35401  satffunlem2  35402  satffun  35403  satefvfmla0  35412  satefvfmla1  35419  fperdvper  45924  ovnovollem1  46661  funressnmo  47051  dfateq12d  47131  afvres  47177  funressndmafv2rn  47228  afv2res  47244  upgrimpths  47913  fdivval  48532  idfth  49151  idsubc  49153