Theorem funeqd 6120

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  Fun wfun 6092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-in 3773  df-ss 3780  df-br 4841  df-opab 4903  df-rel 5315  df-cnv 5316  df-co 5317  df-fun 6100

This theorem is referenced by:  funopg  6132  funsng  6148  f1eq1  6308  f1ssf1  6381  fvn0ssdmfun  6569  funcnvuni  7346  fundmge2nop0  13487  funcnvs2  13878  funcnvs3  13879  funcnvs4  13880  shftfn  14032  isstruct2  16074  structfung  16079  setsfun  16100  setsfun0  16101  strle1  16180  monfval  16592  ismon  16593  monpropd  16597  isepi  16600  isfth  16774  estrresOLD  16979  estrres  16980  lubfun  17181  glbfun  17194  acsficl2d  17377  frlmphl  20326  eengbas  26071  ebtwntg  26072  ecgrtg  26073  elntg  26074  uhgrspansubgrlem  26394  istrl  26817  ispth  26843  isspth  26844  upgrwlkdvspth  26859  uhgrwkspthlem1  26873  uhgrwkspthlem2  26874  usgr2wlkspthlem1  26877  usgr2wlkspthlem2  26878  pthdlem1  26886  2spthd  27077  0spth  27295  3spthd  27345  trlsegvdeglem2  27390  trlsegvdeglem3  27391  ajfun  28041  fresf1o  29757  padct  29821  smatrcl  30184  esum2dlem  30476  omssubadd  30684  sitgf  30731  fperdvper  40610  ovnovollem1  41349  funressnmo  41662  dfateq12d  41712  afvres  41758  funressndmafv2rn  41809  afv2res  41825  fdivval  42898