Theorem rsp 3246

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

Assertion

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

Proof of Theorem rsp

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-ral 3061

This theorem is referenced by:  rspa  3247  rspec  3249  rsp2  3276  r19.12  3313  r19.12OLD  3314  2reu1  3896  reupick2  4330  iuneqconst  5002  iinss2  5056  invdisj  5128  reusv1  5396  reusv2lem1  5397  reusv2lem3  5399  reusv3  5404  ralxfrALT  5414  fvmptss  7027  ffnfv  7138  riota5f  7417  mpoeq123  7506  frrlem4  8315  frrlem8  8319  frrlem10  8321  frrlem13  8324  wfrlem4OLD  8353  wfrlem12OLD  8361  tfr3  8440  tz7.48-1  8484  tz7.49  8486  nneneq  9247  nneneqOLD  9259  frr3g  9797  scottex  9926  dfac2b  10172  infpssrlem4  10347  fin23lem30  10383  fin23lem31  10384  hsmexlem2  10468  domtriomlem  10483  axdc3lem2  10492  axdc3lem4  10494  konigthlem  10609  winalim2  10737  nqereu  10970  dedekind  11425  dedekindle  11426  prodeq2ii  15948  vdwlem9  17028  mreiincl  17640  sgrpidmnd  18753  srgdilem  20190  ringdilem  20247  lbsextlem3  21163  lbsextlem4  21164  tgcl  22977  txindis  23643  alexsubALTlem3  24058  prdsxmslem2  24543  fsumcn  24895  lebnumlem1  24994  iscmet3lem1  25326  iscmet3lem2  25327  ovoliunlem2  25539  mbfimaopnlem  25691  limciun  25930  ftalem3  27119  ostth3  27683  precsexlem10  28241  precsexlem11  28242  mptelee  28911  ubthlem2  30891  aciunf1lem  32673  esumcvg  34088  bnj228  34750  bnj590  34925  bnj594  34927  bnj600  34934  bnj1128  35005  bnj1125  35007  bnj1145  35008  bnj1398  35049  bnj1417  35056  dfon2lem3  35787  dfon2lem7  35791  neibastop1  36361  weiunlem2  36465  unblimceq0lem  36508  unbdqndv2  36513  rdgssun  37380  ralssiun  37409  fvineqsneu  37413  fvineqsneq  37414  cover2  37723  upixp  37737  indexdom  37742  filbcmb  37748  mettrifi  37765  mpobi123f  38170  riotasvd  38958  glbconxN  39381  cdlemefr29exN  40405  cdlemk36  40916  aks4d1p7d1  42084  mptfcl  42736  aomclem2  43072  hbtlem5  43145  gneispace  44152  trintALTVD  44905  trintALT  44906  modelaxrep  45003  refsumcn  45040  rfcnnnub  45046  choicefi  45210  mullimc  45636  mullimcf  45643  addlimc  45668  itgsubsticclem  45995  stoweidlem25  46045  stoweidlem52  46072  stoweidlem59  46079  stoweidlem62  46082  wallispilem3  46087  stirlinglem13  46106  fourierdlem73  46199  natlocalincr  46896  ffnafv  47188  iunord  49250  setrec1lem2  49262