Theorem funeqd 6515

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

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

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 3919  df-br 5100  df-opab 5162  df-rel 5632  df-cnv 5633  df-co 5634  df-fun 6495

This theorem is referenced by:  funopg  6527  funsng  6544  f1eq1  6726  f1ssf1  6807  fvn0ssdmfun  7021  funcnvuni  7876  fundmge2nop0  14429  funcnvs2  14840  funcnvs3  14841  funcnvs4  14842  shftfn  15000  isstruct2  17080  structfung  17085  strle1  17089  setsfun  17102  setsfun0  17103  monfval  17660  ismon  17661  monpropd  17665  isepi  17668  isfth  17844  estrres  18066  lubfun  18277  glbfun  18290  acsficl2d  18479  ebtwntg  29059  ecgrtg  29060  elntg  29061  uhgrspansubgrlem  29367  istrl  29772  ispth  29798  isspth  29799  dfpth2  29806  upgrwlkdvspth  29816  uhgrwkspthlem1  29830  uhgrwkspthlem2  29831  usgr2wlkspthlem1  29834  usgr2wlkspthlem2  29835  pthdlem1  29843  2spthd  30018  0spth  30205  3spthd  30255  trlsegvdeglem2  30300  trlsegvdeglem3  30301  ajfun  30939  fresf1o  32712  padct  32799  smatrcl  33955  esum2dlem  34251  omssubadd  34459  sitgf  34506  funen1cnv  35246  pthhashvtx  35324  satfv0fun  35567  satffunlem1  35603  satffunlem2  35604  satffun  35605  satefvfmla0  35614  satefvfmla1  35621  fperdvper  46230  ovnovollem1  46967  funressnmo  47359  dfateq12d  47439  afvres  47485  funressndmafv2rn  47536  afv2res  47552  upgrimpths  48222  fdivval  48852  idfth  49470  idsubc  49472