Theorem funeqd 6524

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  Fun wfun 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-br 5101  df-opab 5163  df-rel 5641  df-cnv 5642  df-co 5643  df-fun 6504

This theorem is referenced by:  funopg  6536  funsng  6553  f1eq1  6735  f1ssf1  6816  fvn0ssdmfun  7030  funcnvuni  7886  fundmge2nop0  14439  funcnvs2  14850  funcnvs3  14851  funcnvs4  14852  shftfn  15010  isstruct2  17090  structfung  17095  strle1  17099  setsfun  17112  setsfun0  17113  monfval  17670  ismon  17671  monpropd  17675  isepi  17678  isfth  17854  estrres  18076  lubfun  18287  glbfun  18300  acsficl2d  18489  ebtwntg  29073  ecgrtg  29074  elntg  29075  uhgrspansubgrlem  29381  istrl  29786  ispth  29812  isspth  29813  dfpth2  29820  upgrwlkdvspth  29830  uhgrwkspthlem1  29844  uhgrwkspthlem2  29845  usgr2wlkspthlem1  29848  usgr2wlkspthlem2  29849  pthdlem1  29857  2spthd  30032  0spth  30219  3spthd  30269  trlsegvdeglem2  30314  trlsegvdeglem3  30315  ajfun  30954  fresf1o  32727  padct  32814  smatrcl  33980  esum2dlem  34276  omssubadd  34484  sitgf  34531  funen1cnv  35271  pthhashvtx  35350  satfv0fun  35593  satffunlem1  35629  satffunlem2  35630  satffun  35631  satefvfmla0  35640  satefvfmla1  35647  fperdvper  46306  ovnovollem1  47043  funressnmo  47435  dfateq12d  47515  afvres  47561  funressndmafv2rn  47612  afv2res  47628  upgrimpths  48298  fdivval  48928  idfth  49546  idsubc  49548