Theorem rsp 3234

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 2184	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑))
3	1, 2	sylbi 217	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

This theorem is referenced by:  rspa  3235  rspec  3237  rsp2  3263  r19.12  3298  2reu1  3877  reupick2  4311  iuneqconst  4984  iinss2  5038  invdisj  5110  reusv1  5372  reusv2lem1  5373  reusv2lem3  5375  reusv3  5380  ralxfrALT  5390  fvmptss  7003  ffnfv  7114  riota5f  7395  mpoeq123  7484  frrlem4  8293  frrlem8  8297  frrlem10  8299  frrlem13  8302  wfrlem4OLD  8331  wfrlem12OLD  8339  tfr3  8418  tz7.48-1  8462  tz7.49  8464  nneneq  9225  frr3g  9775  scottex  9904  dfac2b  10150  infpssrlem4  10325  fin23lem30  10361  fin23lem31  10362  hsmexlem2  10446  domtriomlem  10461  axdc3lem2  10470  axdc3lem4  10472  konigthlem  10587  winalim2  10715  nqereu  10948  dedekind  11403  dedekindle  11404  prodeq2ii  15932  vdwlem9  17014  mreiincl  17613  sgrpidmnd  18722  srgdilem  20157  ringdilem  20214  lbsextlem3  21126  lbsextlem4  21127  tgcl  22912  txindis  23577  alexsubALTlem3  23992  prdsxmslem2  24473  fsumcn  24817  lebnumlem1  24916  iscmet3lem1  25248  iscmet3lem2  25249  ovoliunlem2  25461  mbfimaopnlem  25613  limciun  25852  ftalem3  27042  ostth3  27606  precsexlem10  28175  precsexlem11  28176  mptelee  28879  ubthlem2  30857  aciunf1lem  32645  esumcvg  34122  bnj228  34771  bnj590  34946  bnj594  34948  bnj600  34955  bnj1128  35026  bnj1125  35028  bnj1145  35029  bnj1398  35070  bnj1417  35077  dfon2lem3  35808  dfon2lem7  35812  neibastop1  36382  weiunlem2  36486  unblimceq0lem  36529  unbdqndv2  36534  rdgssun  37401  ralssiun  37430  fvineqsneu  37434  fvineqsneq  37435  cover2  37744  upixp  37758  indexdom  37763  filbcmb  37769  mettrifi  37786  mpobi123f  38191  riotasvd  38979  glbconxN  39402  cdlemefr29exN  40426  cdlemk36  40937  aks4d1p7d1  42100  mptfcl  42710  aomclem2  43046  hbtlem5  43119  gneispace  44125  trintALTVD  44871  trintALT  44872  modelaxrep  44973  refsumcn  45021  rfcnnnub  45027  choicefi  45191  mullimc  45612  mullimcf  45619  addlimc  45644  itgsubsticclem  45971  stoweidlem25  46021  stoweidlem52  46048  stoweidlem59  46055  stoweidlem62  46058  wallispilem3  46063  stirlinglem13  46082  fourierdlem73  46175  natlocalincr  46872  ffnafv  47167  iunord  49507  setrec1lem2  49519