Theorem funeqd 6247

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522  Fun wfun 6219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-in 3866  df-ss 3874  df-br 4963  df-opab 5025  df-rel 5450  df-cnv 5451  df-co 5452  df-fun 6227

This theorem is referenced by:  funopg  6259  funsng  6275  f1eq1  6438  f1ssf1  6514  fvn0ssdmfun  6707  funcnvuni  7492  fundmge2nop0  13696  funcnvs2  14111  funcnvs3  14112  funcnvs4  14113  shftfn  14266  isstruct2  16322  structfung  16327  setsfun  16347  setsfun0  16348  strle1  16421  monfval  16831  ismon  16832  monpropd  16836  isepi  16839  isfth  17013  estrres  17218  lubfun  17419  glbfun  17432  acsficl2d  17615  frlmphl  20607  ebtwntg  26451  ecgrtg  26452  elntg  26453  uhgrspansubgrlem  26755  istrl  27163  ispth  27191  isspth  27192  upgrwlkdvspth  27207  uhgrwkspthlem1  27221  uhgrwkspthlem2  27222  usgr2wlkspthlem1  27225  usgr2wlkspthlem2  27226  pthdlem1  27234  2spthd  27407  0spth  27592  3spthd  27642  trlsegvdeglem2  27688  trlsegvdeglem3  27689  ajfun  28328  fresf1o  30066  padct  30143  smatrcl  30676  esum2dlem  30968  omssubadd  31175  sitgf  31222  funen1cnv  31971  pthhashvtx  31982  satfv0fun  32226  satffunlem1  32262  satffunlem2  32263  satffun  32264  satefvfmla0  32273  satefvfmla1  32280  fperdvper  41744  ovnovollem1  42480  funressnmo  42797  dfateq12d  42841  afvres  42887  funressndmafv2rn  42938  afv2res  42954  fdivval  44080