Theorem rsp 3220

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-ral 3048

This theorem is referenced by:  rspa  3221  rspec  3223  rsp2  3249  r19.12  3281  2reu1  3843  reupick2  4278  iuneqconst  4951  iinss2  5004  invdisj  5075  reusv1  5333  reusv2lem1  5334  reusv2lem3  5336  reusv3  5341  ralxfrALT  5351  fvmptss  6941  ffnfv  7052  riota5f  7331  mpoeq123  7418  frrlem4  8219  frrlem8  8223  frrlem10  8225  frrlem13  8228  tfr3  8318  tz7.48-1  8362  tz7.49  8364  nneneq  9115  frr3g  9649  scottex  9778  dfac2b  10022  infpssrlem4  10197  fin23lem30  10233  fin23lem31  10234  hsmexlem2  10318  domtriomlem  10333  axdc3lem2  10342  axdc3lem4  10344  konigthlem  10459  winalim2  10587  nqereu  10820  dedekind  11276  dedekindle  11277  prodeq2ii  15818  vdwlem9  16901  mreiincl  17498  sgrpidmnd  18647  srgdilem  20110  ringdilem  20167  lbsextlem3  21097  lbsextlem4  21098  tgcl  22884  txindis  23549  alexsubALTlem3  23964  prdsxmslem2  24444  fsumcn  24788  lebnumlem1  24887  iscmet3lem1  25218  iscmet3lem2  25219  ovoliunlem2  25431  mbfimaopnlem  25583  limciun  25822  ftalem3  27012  ostth3  27576  precsexlem10  28154  precsexlem11  28155  zs12zodd  28392  mptelee  28873  ubthlem2  30851  aciunf1lem  32644  esumcvg  34099  bnj228  34747  bnj590  34922  bnj594  34924  bnj600  34931  bnj1128  35002  bnj1125  35004  bnj1145  35005  bnj1398  35046  bnj1417  35053  dfon2lem3  35827  dfon2lem7  35831  neibastop1  36401  weiunlem2  36505  unblimceq0lem  36548  unbdqndv2  36553  rdgssun  37420  ralssiun  37449  fvineqsneu  37453  fvineqsneq  37454  cover2  37763  upixp  37777  indexdom  37782  filbcmb  37788  mettrifi  37805  mpobi123f  38210  riotasvd  39003  glbconxN  39425  cdlemefr29exN  40449  cdlemk36  40960  aks4d1p7d1  42123  mptfcl  42761  aomclem2  43096  hbtlem5  43169  gneispace  44175  trintALTVD  44920  trintALT  44921  modelaxrep  45022  refsumcn  45075  rfcnnnub  45081  choicefi  45245  mullimc  45664  mullimcf  45671  addlimc  45694  itgsubsticclem  46021  stoweidlem25  46071  stoweidlem52  46098  stoweidlem59  46105  stoweidlem62  46108  wallispilem3  46113  stirlinglem13  46132  fourierdlem73  46225  natlocalincr  46922  ffnafv  47210  iunord  49716  setrec1lem2  49728