Theorem funeqd 6516

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

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

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 3907  df-br 5087  df-opab 5149  df-rel 5633  df-cnv 5634  df-co 5635  df-fun 6496

This theorem is referenced by:  funopg  6528  funsng  6545  f1eq1  6727  f1ssf1  6808  fvn0ssdmfun  7022  funcnvuni  7878  fundmge2nop0  14459  funcnvs2  14870  funcnvs3  14871  funcnvs4  14872  shftfn  15030  isstruct2  17114  structfung  17119  strle1  17123  setsfun  17136  setsfun0  17137  monfval  17694  ismon  17695  monpropd  17699  isepi  17702  isfth  17878  estrres  18100  lubfun  18311  glbfun  18324  acsficl2d  18513  ebtwntg  29069  ecgrtg  29070  elntg  29071  uhgrspansubgrlem  29377  istrl  29782  ispth  29808  isspth  29809  dfpth2  29816  upgrwlkdvspth  29826  uhgrwkspthlem1  29840  uhgrwkspthlem2  29841  usgr2wlkspthlem1  29844  usgr2wlkspthlem2  29845  pthdlem1  29853  2spthd  30028  0spth  30215  3spthd  30265  trlsegvdeglem2  30310  trlsegvdeglem3  30311  ajfun  30950  fresf1o  32723  padct  32810  smatrcl  33960  esum2dlem  34256  omssubadd  34464  sitgf  34511  funen1cnv  35251  pthhashvtx  35330  satfv0fun  35573  satffunlem1  35609  satffunlem2  35610  satffun  35611  satefvfmla0  35620  satefvfmla1  35627  fperdvper  46369  ovnovollem1  47106  funressnmo  47510  dfateq12d  47590  afvres  47636  funressndmafv2rn  47687  afv2res  47703  upgrimpths  48401  fdivval  49031  idfth  49649  idsubc  49651