Theorem funeqd 6559

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  Fun wfun 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5114  df-opab 5178  df-rel 5669  df-cnv 5670  df-co 5671  df-fun 6539

This theorem is referenced by:  funopg  6571  funsng  6588  f1eq1  6770  f1ssf1  6854  fvn0ssdmfun  7070  funcnvuni  7929  fundmge2nop0  14539  funcnvs2  14950  funcnvs3  14951  funcnvs4  14952  shftfn  15110  isstruct2  17209  structfung  17214  strle1  17218  setsfun  17231  setsfun0  17232  monfval  17789  ismon  17790  monpropd  17794  isepi  17797  isfth  17973  estrres  18195  lubfun  18406  glbfun  18419  acsficl2d  18608  ebtwntg  29273  ecgrtg  29274  elntg  29275  uhgrspansubgrlem  29581  istrl  29985  ispth  30011  isspth  30012  dfpth2  30019  upgrwlkdvspth  30029  uhgrwkspthlem1  30043  uhgrwkspthlem2  30044  usgr2wlkspthlem1  30047  usgr2wlkspthlem2  30048  pthdlem1  30056  2spthd  30231  0spth  30418  3spthd  30468  trlsegvdeglem2  30513  trlsegvdeglem3  30514  ajfun  31153  fresf1o  32917  padct  33004  smatrcl  34131  esum2dlem  34427  omssubadd  34635  sitgf  34682  funen1cnv  35420  pthhashvtx  35553  satfv0fun  35796  satffunlem1  35832  satffunlem2  35833  satffun  35834  satefvfmla0  35843  satefvfmla1  35850  fperdvper  46559  ovnovollem1  47296  funressnmo  47706  dfateq12d  47786  afvres  47832  funressndmafv2rn  47883  afv2res  47899  upgrimpths  48597  fdivval  49238  idfth  49855  idsubc  49857