Theorem funeqd 6506

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  Fun wfun 6473

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915  df-br 5093  df-opab 5155  df-rel 5627  df-cnv 5628  df-co 5629  df-fun 6481

This theorem is referenced by:  funopg  6518  funsng  6535  f1eq1  6716  f1ssf1  6799  fvn0ssdmfun  7008  funcnvuni  7846  fundmge2nop0  14306  funcnvs2  14725  funcnvs3  14726  funcnvs4  14727  shftfn  14883  isstruct2  16947  structfung  16952  strle1  16956  setsfun  16969  setsfun0  16970  monfval  17541  ismon  17542  monpropd  17546  isepi  17549  isfth  17727  estrres  17953  lubfun  18167  glbfun  18180  acsficl2d  18367  frlmphl  21094  ebtwntg  27639  ecgrtg  27640  elntg  27641  uhgrspansubgrlem  27946  istrl  28352  ispth  28379  isspth  28380  upgrwlkdvspth  28395  uhgrwkspthlem1  28409  uhgrwkspthlem2  28410  usgr2wlkspthlem1  28413  usgr2wlkspthlem2  28414  pthdlem1  28422  2spthd  28594  0spth  28778  3spthd  28828  trlsegvdeglem2  28873  trlsegvdeglem3  28874  ajfun  29510  fresf1o  31253  padct  31341  smatrcl  32044  esum2dlem  32358  omssubadd  32567  sitgf  32614  funen1cnv  33359  pthhashvtx  33388  satfv0fun  33632  satffunlem1  33668  satffunlem2  33669  satffun  33670  satefvfmla0  33679  satefvfmla1  33686  fperdvper  43804  ovnovollem1  44539  funressnmo  44899  dfateq12d  44977  afvres  45023  funressndmafv2rn  45074  afv2res  45090  fdivval  46244