Theorem rsp 3223

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

Assertion

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

Proof of Theorem rsp

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

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

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 3045

This theorem is referenced by:  rspa  3224  rspec  3226  rsp2  3252  r19.12  3285  2reu1  3857  reupick2  4290  iuneqconst  4963  iinss2  5016  invdisj  5088  reusv1  5347  reusv2lem1  5348  reusv2lem3  5350  reusv3  5355  ralxfrALT  5365  fvmptss  6962  ffnfv  7073  riota5f  7354  mpoeq123  7441  frrlem4  8245  frrlem8  8249  frrlem10  8251  frrlem13  8254  tfr3  8344  tz7.48-1  8388  tz7.49  8390  nneneq  9147  frr3g  9685  scottex  9814  dfac2b  10060  infpssrlem4  10235  fin23lem30  10271  fin23lem31  10272  hsmexlem2  10356  domtriomlem  10371  axdc3lem2  10380  axdc3lem4  10382  konigthlem  10497  winalim2  10625  nqereu  10858  dedekind  11313  dedekindle  11314  prodeq2ii  15853  vdwlem9  16936  mreiincl  17533  sgrpidmnd  18642  srgdilem  20077  ringdilem  20134  lbsextlem3  21046  lbsextlem4  21047  tgcl  22832  txindis  23497  alexsubALTlem3  23912  prdsxmslem2  24393  fsumcn  24737  lebnumlem1  24836  iscmet3lem1  25167  iscmet3lem2  25168  ovoliunlem2  25380  mbfimaopnlem  25532  limciun  25771  ftalem3  26961  ostth3  27525  precsexlem10  28094  precsexlem11  28095  mptelee  28798  ubthlem2  30773  aciunf1lem  32559  esumcvg  34049  bnj228  34698  bnj590  34873  bnj594  34875  bnj600  34882  bnj1128  34953  bnj1125  34955  bnj1145  34956  bnj1398  34997  bnj1417  35004  dfon2lem3  35746  dfon2lem7  35750  neibastop1  36320  weiunlem2  36424  unblimceq0lem  36467  unbdqndv2  36472  rdgssun  37339  ralssiun  37368  fvineqsneu  37372  fvineqsneq  37373  cover2  37682  upixp  37696  indexdom  37701  filbcmb  37707  mettrifi  37724  mpobi123f  38129  riotasvd  38922  glbconxN  39345  cdlemefr29exN  40369  cdlemk36  40880  aks4d1p7d1  42043  mptfcl  42681  aomclem2  43017  hbtlem5  43090  gneispace  44096  trintALTVD  44842  trintALT  44843  modelaxrep  44944  refsumcn  44997  rfcnnnub  45003  choicefi  45167  mullimc  45587  mullimcf  45594  addlimc  45619  itgsubsticclem  45946  stoweidlem25  45996  stoweidlem52  46023  stoweidlem59  46030  stoweidlem62  46033  wallispilem3  46038  stirlinglem13  46057  fourierdlem73  46150  natlocalincr  46847  ffnafv  47145  iunord  49638  setrec1lem2  49650