Theorem rsp 3227

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-ral 3054

This theorem is referenced by:  rspa  3228  rspec  3230  rsp2  3256  r19.12  3288  2reu1  3829  reupick2  4259  iuneqconst  4933  iinss2  4987  invdisj  5058  reusv1  5326  reusv2lem1  5327  reusv2lem3  5329  reusv3  5334  ralxfrALT  5344  fvmptss  6948  ffnfv  7060  riota5f  7341  mpoeq123  7428  frrlem4  8229  frrlem8  8233  frrlem10  8235  frrlem13  8238  tfr3  8328  tz7.48-1  8372  tz7.49  8374  nneneq  9130  frr3g  9671  scottex  9800  dfac2b  10044  infpssrlem4  10219  fin23lem30  10255  fin23lem31  10256  hsmexlem2  10340  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  konigthlem  10482  winalim2  10610  nqereu  10843  dedekind  11300  dedekindle  11301  prodeq2ii  15867  vdwlem9  16951  mreiincl  17549  sgrpidmnd  18698  srgdilem  20164  ringdilem  20221  lbsextlem3  21153  lbsextlem4  21154  tgcl  22952  txindis  23617  alexsubALTlem3  24032  prdsxmslem2  24512  fsumcn  24855  lebnumlem1  24946  iscmet3lem1  25276  iscmet3lem2  25277  ovoliunlem2  25488  mbfimaopnlem  25640  limciun  25879  ftalem3  27056  ostth3  27619  precsexlem10  28226  precsexlem11  28227  z12zsodd  28492  mpteleeOLD  28982  ubthlem2  30960  aciunf1lem  32754  esumcvg  34270  bnj228  34918  bnj590  35092  bnj594  35094  bnj600  35101  bnj1128  35172  bnj1125  35174  bnj1145  35175  bnj1398  35216  bnj1417  35223  dfon2lem3  36011  dfon2lem7  36015  neibastop1  36587  weiunlem  36691  unblimceq0lem  36812  unbdqndv2  36817  rdgssun  37740  ralssiun  37769  fvineqsneu  37773  fvineqsneq  37774  cover2  38082  upixp  38096  indexdom  38101  filbcmb  38107  mettrifi  38124  mpobi123f  38529  rsp3  38733  riotasvd  39448  glbconxN  39870  cdlemefr29exN  40894  cdlemk36  41405  aks4d1p7d1  42567  mptfcl  43169  aomclem2  43500  hbtlem5  43573  gneispace  44578  trintALTVD  45323  trintALT  45324  modelaxrep  45425  refsumcn  45478  rfcnnnub  45484  choicefi  45646  mullimc  46061  mullimcf  46068  addlimc  46091  itgsubsticclem  46418  stoweidlem25  46468  stoweidlem52  46495  stoweidlem59  46502  stoweidlem62  46505  wallispilem3  46510  stirlinglem13  46529  fourierdlem73  46622  natlocalincr  47321  ffnafv  47634  iunord  50166  setrec1lem2  50178