Theorem funeqd 6562

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-rel 5670  df-cnv 5671  df-co 5672  df-fun 6542

This theorem is used by:  funopg  6574  funsng  6591  f1eq1  6773  f1ssf1  6857  fvn0ssdmfun  7073  funcnvuni  7935  funen1cnv  9032  fundmge2nop0  14561  funcnvs2  14978  funcnvs3  14979  funcnvs4  14980  shftfn  15138  isstruct2  17235  structfung  17240  strle1  17244  setsfun  17257  setsfun0  17258  monfval  17815  ismon  17816  monpropd  17820  isepi  17823  isfth  17999  estrres  18221  lubfun  18432  glbfun  18445  acsficl2d  18634  ebtwntg  29391  ecgrtg  29392  elntg  29393  uhgrspansubgrlem  29702  istrl  30110  ispth  30137  isspth  30138  dfpth2  30145  pthhashvtx  30146  upgrwlkdvspth  30156  uhgrwkspthlem1  30170  uhgrwkspthlem2  30171  usgr2wlkspthlem1  30174  usgr2wlkspthlem2  30175  pthdlem1  30183  2spthd  30361  0spth  30548  3spthd  30602  trlsegvdeglem2  30647  trlsegvdeglem3  30648  ajfun  31287  fresf1o  33051  padct  33137  smatrcl  34254  esum2dlem  34550  omssubadd  34759  sitgf  34806  satfv0fun  35904  satffunlem1  35940  satffunlem2  35941  satffun  35942  satefvfmla0  35951  satefvfmla1  35958  fperdvper  46710  ovnovollem1  47447  funressnmo  47860  dfateq12d  47940  afvres  47986  funressndmafv2rn  48037  afv2res  48053  upgrimpths  48751  fdivval  49395  idfth  50012  idsubc  50014