Theorem rsp 3245

Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)

Assertion

Ref	Expression
rsp	⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))

Proof of Theorem rsp

Step	Hyp	Ref	Expression
1		df-ral 3063	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		sp 2177	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑))
3	1, 2	sylbi 216	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-ral 3063

This theorem is referenced by:  rspa  3246  rspec  3248  rsp2  3275  r19.12  3312  r19.12OLD  3313  2reu1  3891  reupick2  4320  rspn0OLD  4353  iuneqconst  5008  iinss2  5060  invdisj  5132  reusv1  5395  reusv2lem1  5396  reusv2lem3  5398  reusv3  5403  ralxfrALT  5413  fvmptss  7008  ffnfv  7115  riota5f  7391  mpoeq123  7478  peano5OLD  7882  frrlem4  8271  frrlem8  8275  frrlem10  8277  frrlem13  8280  wfrlem4OLD  8309  wfrlem12OLD  8317  tfr3  8396  tz7.48-1  8440  tz7.49  8442  nneneq  9206  nneneqOLD  9218  frr3g  9748  scottex  9877  dfac2b  10122  infpssrlem4  10298  fin23lem30  10334  fin23lem31  10335  hsmexlem2  10419  domtriomlem  10434  axdc3lem2  10443  axdc3lem4  10445  konigthlem  10560  winalim2  10688  nqereu  10921  dedekind  11374  dedekindle  11375  prodeq2ii  15854  vdwlem9  16919  mreiincl  17537  sgrpidmnd  18627  srgdilem  20009  ringdilem  20066  lbsextlem3  20766  lbsextlem4  20767  tgcl  22464  txindis  23130  alexsubALTlem3  23545  prdsxmslem2  24030  fsumcn  24378  lebnumlem1  24469  iscmet3lem1  24800  iscmet3lem2  24801  ovoliunlem2  25012  mbfimaopnlem  25164  limciun  25403  ftalem3  26569  ostth3  27131  precsexlem10  27652  precsexlem11  27653  mptelee  28143  ubthlem2  30112  aciunf1lem  31875  esumcvg  33073  bnj228  33735  bnj590  33910  bnj594  33912  bnj600  33919  bnj1128  33990  bnj1125  33992  bnj1145  33993  bnj1398  34034  bnj1417  34041  dfon2lem3  34746  dfon2lem7  34750  neibastop1  35233  unblimceq0lem  35371  unbdqndv2  35376  rdgssun  36248  ralssiun  36277  fvineqsneu  36281  fvineqsneq  36282  cover2  36572  upixp  36586  indexdom  36591  filbcmb  36597  mettrifi  36614  mpobi123f  37019  riotasvd  37815  glbconxN  38238  cdlemefr29exN  39262  cdlemk36  39773  aks4d1p7d1  40936  mptfcl  41444  aomclem2  41783  hbtlem5  41856  gneispace  42871  trintALTVD  43627  trintALT  43628  refsumcn  43700  rfcnnnub  43706  choicefi  43885  mullimc  44319  mullimcf  44326  addlimc  44351  itgsubsticclem  44678  stoweidlem25  44728  stoweidlem52  44755  stoweidlem59  44762  stoweidlem62  44765  wallispilem3  44770  stirlinglem13  44789  fourierdlem73  44882  natlocalincr  45577  ffnafv  45866  iunord  47675  setrec1lem2  47687