Theorem funeqd 6588

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-fun 6563

This theorem is referenced by:  funopg  6600  funsng  6617  f1eq1  6799  f1ssf1  6880  fvn0ssdmfun  7094  funcnvuni  7954  fundmge2nop0  14541  funcnvs2  14952  funcnvs3  14953  funcnvs4  14954  shftfn  15112  isstruct2  17186  structfung  17191  strle1  17195  setsfun  17208  setsfun0  17209  monfval  17776  ismon  17777  monpropd  17781  isepi  17784  isfth  17961  estrres  18184  lubfun  18397  glbfun  18410  acsficl2d  18597  ebtwntg  28997  ecgrtg  28998  elntg  28999  uhgrspansubgrlem  29307  istrl  29714  ispth  29741  isspth  29742  dfpth2  29749  upgrwlkdvspth  29759  uhgrwkspthlem1  29773  uhgrwkspthlem2  29774  usgr2wlkspthlem1  29777  usgr2wlkspthlem2  29778  pthdlem1  29786  2spthd  29961  0spth  30145  3spthd  30195  trlsegvdeglem2  30240  trlsegvdeglem3  30241  ajfun  30879  fresf1o  32641  padct  32731  smatrcl  33795  esum2dlem  34093  omssubadd  34302  sitgf  34349  funen1cnv  35102  pthhashvtx  35133  satfv0fun  35376  satffunlem1  35412  satffunlem2  35413  satffun  35414  satefvfmla0  35423  satefvfmla1  35430  fperdvper  45934  ovnovollem1  46671  funressnmo  47058  dfateq12d  47138  afvres  47184  funressndmafv2rn  47235  afv2res  47251  fdivval  48460