Theorem rsp 3132

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2107  ∀wral 3065

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 3070

This theorem is referenced by:  rspa  3133  rspec  3134  rsp2  3139  r19.12  3258  r19.12OLD  3259  2reu1  3831  reupick2  4255  rspn0OLD  4288  iuneqconst  4936  iinss2  4988  invdisj  5059  reusv1  5321  reusv2lem1  5322  reusv2lem3  5324  reusv3  5329  ralxfrALT  5339  fvmptss  6896  ffnfv  7001  riota5f  7270  mpoeq123  7356  peano5OLD  7750  frrlem4  8114  frrlem8  8118  frrlem10  8120  frrlem13  8123  wfrlem4OLD  8152  wfrlem12OLD  8160  tfr3  8239  tz7.48-1  8283  tz7.49  8285  nneneq  9001  nneneqOLD  9013  frr3g  9523  scottex  9652  dfac2b  9895  infpssrlem4  10071  fin23lem30  10107  fin23lem31  10108  hsmexlem2  10192  domtriomlem  10207  axdc3lem2  10216  axdc3lem4  10218  konigthlem  10333  winalim2  10461  nqereu  10694  dedekind  11147  dedekindle  11148  prodeq2ii  15632  vdwlem9  16699  mreiincl  17314  sgrpidmnd  18399  srgi  19756  ringi  19808  lbsextlem3  20431  lbsextlem4  20432  tgcl  22128  txindis  22794  alexsubALTlem3  23209  prdsxmslem2  23694  fsumcn  24042  lebnumlem1  24133  iscmet3lem1  24464  iscmet3lem2  24465  ovoliunlem2  24676  mbfimaopnlem  24828  limciun  25067  ftalem3  26233  ostth3  26795  mptelee  27272  ubthlem2  29242  aciunf1lem  31008  esumcvg  32063  bnj228  32723  bnj590  32899  bnj594  32901  bnj600  32908  bnj1128  32979  bnj1125  32981  bnj1145  32982  bnj1398  33023  bnj1417  33030  dfon2lem3  33770  dfon2lem7  33774  neibastop1  34557  unblimceq0lem  34695  unbdqndv2  34700  rdgssun  35558  ralssiun  35587  fvineqsneu  35591  fvineqsneq  35592  cover2  35881  upixp  35896  indexdom  35901  filbcmb  35907  mettrifi  35924  mpobi123f  36329  riotasvd  36977  glbconxN  37399  cdlemefr29exN  38423  cdlemk36  38934  aks4d1p7d1  40097  mptfcl  40549  aomclem2  40887  hbtlem5  40960  gneispace  41751  trintALTVD  42507  trintALT  42508  refsumcn  42580  rfcnnnub  42586  choicefi  42747  mullimc  43164  mullimcf  43171  addlimc  43196  itgsubsticclem  43523  stoweidlem25  43573  stoweidlem52  43600  stoweidlem59  43607  stoweidlem62  43610  wallispilem3  43615  stirlinglem13  43634  fourierdlem73  43727  ffnafv  44674  iunord  46393  setrec1lem2  46405  natlocalincr  46522