Theorem rsp 3226

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∀wral 3052

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-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-ral 3053

This theorem is referenced by:  rspa  3227  rspec  3229  rsp2  3255  r19.12  3287  2reu1  3836  reupick2  4272  iuneqconst  4946  iinss2  5001  invdisj  5072  reusv1  5334  reusv2lem1  5335  reusv2lem3  5337  reusv3  5342  ralxfrALT  5352  fvmptss  6954  ffnfv  7065  riota5f  7345  mpoeq123  7432  frrlem4  8232  frrlem8  8236  frrlem10  8238  frrlem13  8241  tfr3  8331  tz7.48-1  8375  tz7.49  8377  nneneq  9133  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  21150  lbsextlem4  21151  tgcl  22944  txindis  23609  alexsubALTlem3  24024  prdsxmslem2  24504  fsumcn  24847  lebnumlem1  24938  iscmet3lem1  25268  iscmet3lem2  25269  ovoliunlem2  25480  mbfimaopnlem  25632  limciun  25871  ftalem3  27052  ostth3  27615  precsexlem10  28222  precsexlem11  28223  z12zsodd  28488  mpteleeOLD  28978  ubthlem2  30957  aciunf1lem  32750  esumcvg  34246  bnj228  34894  bnj590  35068  bnj594  35070  bnj600  35077  bnj1128  35148  bnj1125  35150  bnj1145  35151  bnj1398  35192  bnj1417  35199  dfon2lem3  35981  dfon2lem7  35985  neibastop1  36557  weiunlem  36661  unblimceq0lem  36782  unbdqndv2  36787  rdgssun  37708  ralssiun  37737  fvineqsneu  37741  fvineqsneq  37742  cover2  38050  upixp  38064  indexdom  38069  filbcmb  38075  mettrifi  38092  mpobi123f  38497  rsp3  38701  riotasvd  39416  glbconxN  39838  cdlemefr29exN  40862  cdlemk36  41373  aks4d1p7d1  42535  mptfcl  43166  aomclem2  43501  hbtlem5  43574  gneispace  44579  trintALTVD  45324  trintALT  45325  modelaxrep  45426  refsumcn  45479  rfcnnnub  45485  choicefi  45647  mullimc  46064  mullimcf  46071  addlimc  46094  itgsubsticclem  46421  stoweidlem25  46471  stoweidlem52  46498  stoweidlem59  46505  stoweidlem62  46508  wallispilem3  46513  stirlinglem13  46532  fourierdlem73  46625  natlocalincr  47322  ffnafv  47631  iunord  50163  setrec1lem2  50175