Theorem funeqd 6377

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  Fun wfun 6349

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-br 5067  df-opab 5129  df-rel 5562  df-cnv 5563  df-co 5564  df-fun 6357

This theorem is referenced by:  funopg  6389  funsng  6405  f1eq1  6570  f1ssf1  6646  fvn0ssdmfun  6842  funcnvuni  7636  fundmge2nop0  13851  funcnvs2  14275  funcnvs3  14276  funcnvs4  14277  shftfn  14432  isstruct2  16493  structfung  16498  setsfun  16518  setsfun0  16519  strle1  16592  monfval  17002  ismon  17003  monpropd  17007  isepi  17010  isfth  17184  estrres  17389  lubfun  17590  glbfun  17603  acsficl2d  17786  frlmphl  20925  ebtwntg  26768  ecgrtg  26769  elntg  26770  uhgrspansubgrlem  27072  istrl  27478  ispth  27504  isspth  27505  upgrwlkdvspth  27520  uhgrwkspthlem1  27534  uhgrwkspthlem2  27535  usgr2wlkspthlem1  27538  usgr2wlkspthlem2  27539  pthdlem1  27547  2spthd  27720  0spth  27905  3spthd  27955  trlsegvdeglem2  28000  trlsegvdeglem3  28001  ajfun  28637  fresf1o  30376  padct  30455  smatrcl  31061  esum2dlem  31351  omssubadd  31558  sitgf  31605  funen1cnv  32357  pthhashvtx  32374  satfv0fun  32618  satffunlem1  32654  satffunlem2  32655  satffun  32656  satefvfmla0  32665  satefvfmla1  32672  fperdvper  42223  ovnovollem1  42958  funressnmo  43301  dfateq12d  43345  afvres  43391  funressndmafv2rn  43442  afv2res  43458  fdivval  44619