Theorem rsp 3226

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

Assertion

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

Proof of Theorem rsp

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

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

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 3046

This theorem is referenced by:  rspa  3227  rspec  3229  rsp2  3255  r19.12  3290  2reu1  3863  reupick2  4297  iuneqconst  4970  iinss2  5024  invdisj  5096  reusv1  5355  reusv2lem1  5356  reusv2lem3  5358  reusv3  5363  ralxfrALT  5373  fvmptss  6983  ffnfv  7094  riota5f  7375  mpoeq123  7464  frrlem4  8271  frrlem8  8275  frrlem10  8277  frrlem13  8280  tfr3  8370  tz7.48-1  8414  tz7.49  8416  nneneq  9176  frr3g  9716  scottex  9845  dfac2b  10091  infpssrlem4  10266  fin23lem30  10302  fin23lem31  10303  hsmexlem2  10387  domtriomlem  10402  axdc3lem2  10411  axdc3lem4  10413  konigthlem  10528  winalim2  10656  nqereu  10889  dedekind  11344  dedekindle  11345  prodeq2ii  15884  vdwlem9  16967  mreiincl  17564  sgrpidmnd  18673  srgdilem  20108  ringdilem  20165  lbsextlem3  21077  lbsextlem4  21078  tgcl  22863  txindis  23528  alexsubALTlem3  23943  prdsxmslem2  24424  fsumcn  24768  lebnumlem1  24867  iscmet3lem1  25198  iscmet3lem2  25199  ovoliunlem2  25411  mbfimaopnlem  25563  limciun  25802  ftalem3  26992  ostth3  27556  precsexlem10  28125  precsexlem11  28126  mptelee  28829  ubthlem2  30807  aciunf1lem  32593  esumcvg  34083  bnj228  34732  bnj590  34907  bnj594  34909  bnj600  34916  bnj1128  34987  bnj1125  34989  bnj1145  34990  bnj1398  35031  bnj1417  35038  dfon2lem3  35780  dfon2lem7  35784  neibastop1  36354  weiunlem2  36458  unblimceq0lem  36501  unbdqndv2  36506  rdgssun  37373  ralssiun  37402  fvineqsneu  37406  fvineqsneq  37407  cover2  37716  upixp  37730  indexdom  37735  filbcmb  37741  mettrifi  37758  mpobi123f  38163  riotasvd  38956  glbconxN  39379  cdlemefr29exN  40403  cdlemk36  40914  aks4d1p7d1  42077  mptfcl  42715  aomclem2  43051  hbtlem5  43124  gneispace  44130  trintALTVD  44876  trintALT  44877  modelaxrep  44978  refsumcn  45031  rfcnnnub  45037  choicefi  45201  mullimc  45621  mullimcf  45628  addlimc  45653  itgsubsticclem  45980  stoweidlem25  46030  stoweidlem52  46057  stoweidlem59  46064  stoweidlem62  46067  wallispilem3  46072  stirlinglem13  46091  fourierdlem73  46184  natlocalincr  46881  ffnafv  47176  iunord  49669  setrec1lem2  49681