Theorem funeqd 6503

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  Fun wfun 6475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-br 5090  df-opab 5152  df-rel 5621  df-cnv 5622  df-co 5623  df-fun 6483

This theorem is referenced by:  funopg  6515  funsng  6532  f1eq1  6714  f1ssf1  6795  fvn0ssdmfun  7007  funcnvuni  7862  fundmge2nop0  14409  funcnvs2  14820  funcnvs3  14821  funcnvs4  14822  shftfn  14980  isstruct2  17060  structfung  17065  strle1  17069  setsfun  17082  setsfun0  17083  monfval  17639  ismon  17640  monpropd  17644  isepi  17647  isfth  17823  estrres  18045  lubfun  18256  glbfun  18269  acsficl2d  18458  ebtwntg  28960  ecgrtg  28961  elntg  28962  uhgrspansubgrlem  29268  istrl  29673  ispth  29699  isspth  29700  dfpth2  29707  upgrwlkdvspth  29717  uhgrwkspthlem1  29731  uhgrwkspthlem2  29732  usgr2wlkspthlem1  29735  usgr2wlkspthlem2  29736  pthdlem1  29744  2spthd  29919  0spth  30106  3spthd  30156  trlsegvdeglem2  30201  trlsegvdeglem3  30202  ajfun  30840  fresf1o  32613  padct  32701  smatrcl  33809  esum2dlem  34105  omssubadd  34313  sitgf  34360  funen1cnv  35100  pthhashvtx  35172  satfv0fun  35415  satffunlem1  35451  satffunlem2  35452  satffun  35453  satefvfmla0  35462  satefvfmla1  35469  fperdvper  46016  ovnovollem1  46753  funressnmo  47145  dfateq12d  47225  afvres  47271  funressndmafv2rn  47322  afv2res  47338  upgrimpths  48008  fdivval  48639  idfth  49258  idsubc  49260