Theorem funeqd 6561

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 6559	. 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 6532

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-fun 6540

This theorem is used by:  funopg  6574  funsng  6591  f1eq1  6773  f1ssf1  6857  fvn0ssdmfun  7074  funcnvuni  7944  funen1cnv  9056  fundmge2nop0  14647  funcnvs2  15064  funcnvs3  15065  funcnvs4  15066  shftfn  15226  isstruct2  17327  structfung  17332  strle1  17336  setsfun  17349  setsfun0  17350  monfval  17907  ismon  17908  monpropd  17912  isepi  17915  isfth  18091  estrres  18313  lubfun  18524  glbfun  18537  acsficl2d  18726  ebtwntg  29560  ecgrtg  29561  elntg  29562  uhgrspansubgrlem  29871  istrl  30279  ispth  30306  isspth  30307  dfpth2  30314  pthhashvtx  30315  upgrwlkdvspth  30325  uhgrwkspthlem1  30339  uhgrwkspthlem2  30340  usgr2wlkspthlem1  30343  usgr2wlkspthlem2  30344  pthdlem1  30352  2spthd  30530  0spth  30717  3spthd  30777  trlsegvdeglem2  30822  trlsegvdeglem3  30823  ajfun  31462  fresf1o  33225  padct  33310  smatrcl  34428  esum2dlem  34724  omssubadd  34932  sitgf  34979  satfv0fun  36136  satffunlem1  36172  satffunlem2  36173  satffun  36174  satefvfmla0  36183  satefvfmla1  36190  hfstructfun  46025  fperdvper  46928  ovnovollem1  47665  tmachlem-agreefin  47957  funressnmo  48115  dfateq12d  48195  afvres  48241  funressndmafv2rn  48292  afv2res  48308  upgrimpths  49006  fdivval  49650  idfth  50265  idsubc  50267