Theorem rsp 3222

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  ∀wral 3049

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 2182

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

This theorem is referenced by:  rspa  3223  rspec  3225  rsp2  3251  r19.12  3283  2reu1  3845  reupick2  4281  iuneqconst  4956  iinss2  5011  invdisj  5082  reusv1  5340  reusv2lem1  5341  reusv2lem3  5343  reusv3  5348  ralxfrALT  5358  fvmptss  6951  ffnfv  7062  riota5f  7341  mpoeq123  7428  frrlem4  8229  frrlem8  8233  frrlem10  8235  frrlem13  8238  tfr3  8328  tz7.48-1  8372  tz7.49  8374  nneneq  9128  frr3g  9666  scottex  9795  dfac2b  10039  infpssrlem4  10214  fin23lem30  10250  fin23lem31  10251  hsmexlem2  10335  domtriomlem  10350  axdc3lem2  10359  axdc3lem4  10361  konigthlem  10477  winalim2  10605  nqereu  10838  dedekind  11294  dedekindle  11295  prodeq2ii  15832  vdwlem9  16915  mreiincl  17513  sgrpidmnd  18662  srgdilem  20125  ringdilem  20182  lbsextlem3  21113  lbsextlem4  21114  tgcl  22911  txindis  23576  alexsubALTlem3  23991  prdsxmslem2  24471  fsumcn  24815  lebnumlem1  24914  iscmet3lem1  25245  iscmet3lem2  25246  ovoliunlem2  25458  mbfimaopnlem  25610  limciun  25849  ftalem3  27039  ostth3  27603  precsexlem10  28184  precsexlem11  28185  zs12zodd  28431  mpteleeOLD  28917  ubthlem2  30895  aciunf1lem  32689  esumcvg  34192  bnj228  34840  bnj590  35015  bnj594  35017  bnj600  35024  bnj1128  35095  bnj1125  35097  bnj1145  35098  bnj1398  35139  bnj1417  35146  dfon2lem3  35926  dfon2lem7  35930  neibastop1  36502  weiunlem2  36606  unblimceq0lem  36649  unbdqndv2  36654  rdgssun  37522  ralssiun  37551  fvineqsneu  37555  fvineqsneq  37556  cover2  37855  upixp  37869  indexdom  37874  filbcmb  37880  mettrifi  37897  mpobi123f  38302  riotasvd  39155  glbconxN  39577  cdlemefr29exN  40601  cdlemk36  41112  aks4d1p7d1  42275  mptfcl  42904  aomclem2  43239  hbtlem5  43312  gneispace  44317  trintALTVD  45062  trintALT  45063  modelaxrep  45164  refsumcn  45217  rfcnnnub  45223  choicefi  45386  mullimc  45804  mullimcf  45811  addlimc  45834  itgsubsticclem  46161  stoweidlem25  46211  stoweidlem52  46238  stoweidlem59  46245  stoweidlem62  46248  wallispilem3  46253  stirlinglem13  46272  fourierdlem73  46365  natlocalincr  47062  ffnafv  47359  iunord  49863  setrec1lem2  49875