Theorem funeqd 6520

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-fun 6500

This theorem is referenced by:  funopg  6532  funsng  6549  f1eq1  6731  f1ssf1  6812  fvn0ssdmfun  7026  funcnvuni  7883  fundmge2nop0  14464  funcnvs2  14875  funcnvs3  14876  funcnvs4  14877  shftfn  15035  isstruct2  17119  structfung  17124  strle1  17128  setsfun  17141  setsfun0  17142  monfval  17699  ismon  17700  monpropd  17704  isepi  17707  isfth  17883  estrres  18105  lubfun  18316  glbfun  18329  acsficl2d  18518  ebtwntg  29051  ecgrtg  29052  elntg  29053  uhgrspansubgrlem  29359  istrl  29763  ispth  29789  isspth  29790  dfpth2  29797  upgrwlkdvspth  29807  uhgrwkspthlem1  29821  uhgrwkspthlem2  29822  usgr2wlkspthlem1  29825  usgr2wlkspthlem2  29826  pthdlem1  29834  2spthd  30009  0spth  30196  3spthd  30246  trlsegvdeglem2  30291  trlsegvdeglem3  30292  ajfun  30931  fresf1o  32704  padct  32791  smatrcl  33940  esum2dlem  34236  omssubadd  34444  sitgf  34491  funen1cnv  35231  pthhashvtx  35310  satfv0fun  35553  satffunlem1  35589  satffunlem2  35590  satffun  35591  satefvfmla0  35600  satefvfmla1  35607  fperdvper  46347  ovnovollem1  47084  funressnmo  47494  dfateq12d  47574  afvres  47620  funressndmafv2rn  47671  afv2res  47687  upgrimpths  48385  fdivval  49015  idfth  49633  idsubc  49635