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  18648  srgdilem  20112  ringdilem  20169  lbsextlem3  21102  lbsextlem4  21103  tgcl  22889  txindis  23554  alexsubALTlem3  23969  prdsxmslem2  24450  fsumcn  24794  lebnumlem1  24893  iscmet3lem1  25224  iscmet3lem2  25225  ovoliunlem2  25437  mbfimaopnlem  25589  limciun  25828  ftalem3  27018  ostth3  27582  precsexlem10  28158  precsexlem11  28159  zs12zodd  28394  mptelee  28875  ubthlem2  30850  aciunf1lem  32636  esumcvg  34069  bnj228  34718  bnj590  34893  bnj594  34895  bnj600  34902  bnj1128  34973  bnj1125  34975  bnj1145  34976  bnj1398  35017  bnj1417  35024  dfon2lem3  35766  dfon2lem7  35770  neibastop1  36340  weiunlem2  36444  unblimceq0lem  36487  unbdqndv2  36492  rdgssun  37359  ralssiun  37388  fvineqsneu  37392  fvineqsneq  37393  cover2  37702  upixp  37716  indexdom  37721  filbcmb  37727  mettrifi  37744  mpobi123f  38149  riotasvd  38942  glbconxN  39365  cdlemefr29exN  40389  cdlemk36  40900  aks4d1p7d1  42063  mptfcl  42701  aomclem2  43037  hbtlem5  43110  gneispace  44116  trintALTVD  44862  trintALT  44863  modelaxrep  44964  refsumcn  45017  rfcnnnub  45023  choicefi  45187  mullimc  45607  mullimcf  45614  addlimc  45639  itgsubsticclem  45966  stoweidlem25  46016  stoweidlem52  46043  stoweidlem59  46050  stoweidlem62  46053  wallispilem3  46058  stirlinglem13  46077  fourierdlem73  46170  natlocalincr  46867  ffnafv  47165  iunord  49658  setrec1lem2  49670