Theorem funeqd 6555

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 6553	. 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 6527

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-fun 6535

This theorem is used by:  funopg  6568  funsng  6585  f1eq1  6767  f1ssf1  6851  fvn0ssdmfun  7068  funcnvuni  7930  funen1cnv  9038  fundmge2nop0  14570  funcnvs2  14987  funcnvs3  14988  funcnvs4  14989  shftfn  15149  isstruct2  17244  structfung  17249  strle1  17253  setsfun  17266  setsfun0  17267  monfval  17824  ismon  17825  monpropd  17829  isepi  17832  isfth  18008  estrres  18230  lubfun  18441  glbfun  18454  acsficl2d  18643  ebtwntg  29442  ecgrtg  29443  elntg  29444  uhgrspansubgrlem  29753  istrl  30161  ispth  30188  isspth  30189  dfpth2  30196  pthhashvtx  30197  upgrwlkdvspth  30207  uhgrwkspthlem1  30221  uhgrwkspthlem2  30222  usgr2wlkspthlem1  30225  usgr2wlkspthlem2  30226  pthdlem1  30234  2spthd  30412  0spth  30599  3spthd  30659  trlsegvdeglem2  30704  trlsegvdeglem3  30705  ajfun  31344  fresf1o  33107  padct  33192  smatrcl  34309  esum2dlem  34605  omssubadd  34814  sitgf  34861  satfv0fun  35953  satffunlem1  35989  satffunlem2  35990  satffun  35991  satefvfmla0  36000  satefvfmla1  36007  fperdvper  46750  ovnovollem1  47487  tmachlem-agreefin  47779  funressnmo  47937  dfateq12d  48017  afvres  48063  funressndmafv2rn  48114  afv2res  48130  upgrimpths  48828  fdivval  49472  idfth  50087  idsubc  50089