Theorem rsp 3224

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-ral 3052

This theorem is referenced by:  rspa  3225  rspec  3227  rsp2  3253  r19.12  3285  2reu1  3847  reupick2  4283  iuneqconst  4958  iinss2  5013  invdisj  5084  reusv1  5342  reusv2lem1  5343  reusv2lem3  5345  reusv3  5350  ralxfrALT  5360  fvmptss  6953  ffnfv  7064  riota5f  7343  mpoeq123  7430  frrlem4  8231  frrlem8  8235  frrlem10  8237  frrlem13  8240  tfr3  8330  tz7.48-1  8374  tz7.49  8376  nneneq  9130  frr3g  9668  scottex  9797  dfac2b  10041  infpssrlem4  10216  fin23lem30  10252  fin23lem31  10253  hsmexlem2  10337  domtriomlem  10352  axdc3lem2  10361  axdc3lem4  10363  konigthlem  10479  winalim2  10607  nqereu  10840  dedekind  11296  dedekindle  11297  prodeq2ii  15834  vdwlem9  16917  mreiincl  17515  sgrpidmnd  18664  srgdilem  20127  ringdilem  20184  lbsextlem3  21115  lbsextlem4  21116  tgcl  22913  txindis  23578  alexsubALTlem3  23993  prdsxmslem2  24473  fsumcn  24817  lebnumlem1  24916  iscmet3lem1  25247  iscmet3lem2  25248  ovoliunlem2  25460  mbfimaopnlem  25612  limciun  25851  ftalem3  27041  ostth3  27605  precsexlem10  28212  precsexlem11  28213  z12zsodd  28478  mpteleeOLD  28968  ubthlem2  30946  aciunf1lem  32740  esumcvg  34243  bnj228  34891  bnj590  35066  bnj594  35068  bnj600  35075  bnj1128  35146  bnj1125  35148  bnj1145  35149  bnj1398  35190  bnj1417  35197  dfon2lem3  35977  dfon2lem7  35981  neibastop1  36553  weiunlem  36657  unblimceq0lem  36706  unbdqndv2  36711  rdgssun  37583  ralssiun  37612  fvineqsneu  37616  fvineqsneq  37617  cover2  37916  upixp  37930  indexdom  37935  filbcmb  37941  mettrifi  37958  mpobi123f  38363  riotasvd  39216  glbconxN  39638  cdlemefr29exN  40662  cdlemk36  41173  aks4d1p7d1  42336  mptfcl  42962  aomclem2  43297  hbtlem5  43370  gneispace  44375  trintALTVD  45120  trintALT  45121  modelaxrep  45222  refsumcn  45275  rfcnnnub  45281  choicefi  45444  mullimc  45862  mullimcf  45869  addlimc  45892  itgsubsticclem  46219  stoweidlem25  46269  stoweidlem52  46296  stoweidlem59  46303  stoweidlem62  46306  wallispilem3  46311  stirlinglem13  46330  fourierdlem73  46423  natlocalincr  47120  ffnafv  47417  iunord  49921  setrec1lem2  49933