Theorem funeqd 6402

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  Fun wfun 6374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-br 5054  df-opab 5116  df-rel 5558  df-cnv 5559  df-co 5560  df-fun 6382

This theorem is referenced by:  funopg  6414  funsng  6431  f1eq1  6610  f1ssf1  6692  fvn0ssdmfun  6895  funcnvuni  7709  fundmge2nop0  14058  funcnvs2  14478  funcnvs3  14479  funcnvs4  14480  shftfn  14636  isstruct2  16702  structfung  16707  strle1  16711  setsfun  16724  setsfun0  16725  monfval  17237  ismon  17238  monpropd  17242  isepi  17245  isfth  17421  estrres  17646  lubfun  17858  glbfun  17871  acsficl2d  18058  frlmphl  20743  ebtwntg  27073  ecgrtg  27074  elntg  27075  uhgrspansubgrlem  27378  istrl  27784  ispth  27810  isspth  27811  upgrwlkdvspth  27826  uhgrwkspthlem1  27840  uhgrwkspthlem2  27841  usgr2wlkspthlem1  27844  usgr2wlkspthlem2  27845  pthdlem1  27853  2spthd  28025  0spth  28209  3spthd  28259  trlsegvdeglem2  28304  trlsegvdeglem3  28305  ajfun  28941  fresf1o  30685  padct  30774  smatrcl  31460  esum2dlem  31772  omssubadd  31979  sitgf  32026  funen1cnv  32773  pthhashvtx  32802  satfv0fun  33046  satffunlem1  33082  satffunlem2  33083  satffun  33084  satefvfmla0  33093  satefvfmla1  33100  fperdvper  43135  ovnovollem1  43869  funressnmo  44212  dfateq12d  44290  afvres  44336  funressndmafv2rn  44387  afv2res  44403  fdivval  45558