Theorem funeqd 6570

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5107  df-opab 5171  df-rel 5662  df-cnv 5663  df-co 5664  df-fun 6549

This theorem is used by:  funopg  6583  funsng  6602  f1eq1  6784  f1ssf1  6868  fvn0ssdmfun  7085  funcnvuni  7954  funen1cnv  9070  fundmge2nop0  14660  funcnvs2  15079  funcnvs3  15080  funcnvs4  15081  shftfn  15241  isstruct2  17342  structfung  17347  strle1  17351  setsfun  17364  setsfun0  17365  monfval  17922  ismon  17923  monpropd  17927  isepi  17930  isfth  18106  estrres  18328  lubfun  18539  glbfun  18552  acsficl2d  18741  ebtwntg  29575  ecgrtg  29576  elntg  29577  uhgrspansubgrlem  29886  istrl  30294  ispth  30321  isspth  30322  dfpth2  30329  pthhashvtx  30330  upgrwlkdvspth  30340  uhgrwkspthlem1  30354  uhgrwkspthlem2  30355  usgr2wlkspthlem1  30358  usgr2wlkspthlem2  30359  pthdlem1  30367  2spthd  30545  0spth  30732  3spthd  30792  trlsegvdeglem2  30837  trlsegvdeglem3  30838  ajfun  31477  fresf1o  33282  padct  33367  smatrcl  34484  esum2dlem  34780  omssubadd  34988  sitgf  35035  satfv0fun  36260  satffunlem1  36296  satffunlem2  36297  satffun  36298  satefvfmla0  36307  satefvfmla1  36314  hfstructfun  46171  fperdvper  47074  ovnovollem1  47811  tmachlem-agreefin  48103  funressnmo  48261  dfateq12d  48341  afvres  48387  funressndmafv2rn  48438  afv2res  48454  upgrimpths  49152  fdivval  49796  idfth  50419  idsubc  50421