Theorem rsp 3253

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-ral 3068

This theorem is referenced by:  rspa  3254  rspec  3256  rsp2  3283  r19.12  3320  r19.12OLD  3321  2reu1  3919  reupick2  4350  iuneqconst  5026  iinss2  5080  invdisj  5152  reusv1  5415  reusv2lem1  5416  reusv2lem3  5418  reusv3  5423  ralxfrALT  5433  fvmptss  7041  ffnfv  7153  riota5f  7433  mpoeq123  7522  peano5OLD  7933  frrlem4  8330  frrlem8  8334  frrlem10  8336  frrlem13  8339  wfrlem4OLD  8368  wfrlem12OLD  8376  tfr3  8455  tz7.48-1  8499  tz7.49  8501  nneneq  9272  nneneqOLD  9284  frr3g  9825  scottex  9954  dfac2b  10200  infpssrlem4  10375  fin23lem30  10411  fin23lem31  10412  hsmexlem2  10496  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  konigthlem  10637  winalim2  10765  nqereu  10998  dedekind  11453  dedekindle  11454  prodeq2ii  15959  vdwlem9  17036  mreiincl  17654  sgrpidmnd  18777  srgdilem  20219  ringdilem  20276  lbsextlem3  21185  lbsextlem4  21186  tgcl  22997  txindis  23663  alexsubALTlem3  24078  prdsxmslem2  24563  fsumcn  24913  lebnumlem1  25012  iscmet3lem1  25344  iscmet3lem2  25345  ovoliunlem2  25557  mbfimaopnlem  25709  limciun  25949  ftalem3  27136  ostth3  27700  precsexlem10  28258  precsexlem11  28259  mptelee  28928  ubthlem2  30903  aciunf1lem  32680  esumcvg  34050  bnj228  34711  bnj590  34886  bnj594  34888  bnj600  34895  bnj1128  34966  bnj1125  34968  bnj1145  34969  bnj1398  35010  bnj1417  35017  dfon2lem3  35749  dfon2lem7  35753  neibastop1  36325  weiunlem2  36429  unblimceq0lem  36472  unbdqndv2  36477  rdgssun  37344  ralssiun  37373  fvineqsneu  37377  fvineqsneq  37378  cover2  37675  upixp  37689  indexdom  37694  filbcmb  37700  mettrifi  37717  mpobi123f  38122  riotasvd  38912  glbconxN  39335  cdlemefr29exN  40359  cdlemk36  40870  aks4d1p7d1  42039  mptfcl  42676  aomclem2  43012  hbtlem5  43085  gneispace  44096  trintALTVD  44851  trintALT  44852  refsumcn  44930  rfcnnnub  44936  choicefi  45107  mullimc  45537  mullimcf  45544  addlimc  45569  itgsubsticclem  45896  stoweidlem25  45946  stoweidlem52  45973  stoweidlem59  45980  stoweidlem62  45983  wallispilem3  45988  stirlinglem13  46007  fourierdlem73  46100  natlocalincr  46795  ffnafv  47086  iunord  48768  setrec1lem2  48780