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 17	1 ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-rel 5661  df-cnv 5662  df-co 5663  df-fun 6533

This theorem is referenced by:  funopg  6570  funsng  6587  f1eq1  6769  f1ssf1  6850  fvn0ssdmfun  7064  funcnvuni  7928  fundmge2nop0  14520  funcnvs2  14932  funcnvs3  14933  funcnvs4  14934  shftfn  15092  isstruct2  17168  structfung  17173  strle1  17177  setsfun  17190  setsfun0  17191  monfval  17745  ismon  17746  monpropd  17750  isepi  17753  isfth  17929  estrres  18151  lubfun  18362  glbfun  18375  acsficl2d  18562  ebtwntg  28961  ecgrtg  28962  elntg  28963  uhgrspansubgrlem  29269  istrl  29676  ispth  29703  isspth  29704  dfpth2  29711  upgrwlkdvspth  29721  uhgrwkspthlem1  29735  uhgrwkspthlem2  29736  usgr2wlkspthlem1  29739  usgr2wlkspthlem2  29740  pthdlem1  29748  2spthd  29923  0spth  30107  3spthd  30157  trlsegvdeglem2  30202  trlsegvdeglem3  30203  ajfun  30841  fresf1o  32609  padct  32697  smatrcl  33827  esum2dlem  34123  omssubadd  34332  sitgf  34379  funen1cnv  35119  pthhashvtx  35150  satfv0fun  35393  satffunlem1  35429  satffunlem2  35430  satffun  35431  satefvfmla0  35440  satefvfmla1  35447  fperdvper  45948  ovnovollem1  46685  funressnmo  47075  dfateq12d  47155  afvres  47201  funressndmafv2rn  47252  afv2res  47268  upgrimpths  47922  fdivval  48519  idfth  49098  idsubc  49099