Theorem rsp 3225

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-ral 3052

This theorem is referenced by:  rspa  3226  rspec  3228  rsp2  3254  r19.12  3286  2reu1  3835  reupick2  4271  iuneqconst  4945  iinss2  5000  invdisj  5071  reusv1  5339  reusv2lem1  5340  reusv2lem3  5342  reusv3  5347  ralxfrALT  5357  fvmptss  6960  ffnfv  7071  riota5f  7352  mpoeq123  7439  frrlem4  8239  frrlem8  8243  frrlem10  8245  frrlem13  8248  tfr3  8338  tz7.48-1  8382  tz7.49  8384  nneneq  9140  frr3g  9680  scottex  9809  dfac2b  10053  infpssrlem4  10228  fin23lem30  10264  fin23lem31  10265  hsmexlem2  10349  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  konigthlem  10491  winalim2  10619  nqereu  10852  dedekind  11309  dedekindle  11310  prodeq2ii  15876  vdwlem9  16960  mreiincl  17558  sgrpidmnd  18707  srgdilem  20173  ringdilem  20230  lbsextlem3  21158  lbsextlem4  21159  tgcl  22934  txindis  23599  alexsubALTlem3  24014  prdsxmslem2  24494  fsumcn  24837  lebnumlem1  24928  iscmet3lem1  25258  iscmet3lem2  25259  ovoliunlem2  25470  mbfimaopnlem  25622  limciun  25861  ftalem3  27038  ostth3  27601  precsexlem10  28208  precsexlem11  28209  z12zsodd  28474  mpteleeOLD  28964  ubthlem2  30942  aciunf1lem  32735  esumcvg  34230  bnj228  34878  bnj590  35052  bnj594  35054  bnj600  35061  bnj1128  35132  bnj1125  35134  bnj1145  35135  bnj1398  35176  bnj1417  35183  dfon2lem3  35965  dfon2lem7  35969  neibastop1  36541  weiunlem  36645  unblimceq0lem  36766  unbdqndv2  36771  rdgssun  37694  ralssiun  37723  fvineqsneu  37727  fvineqsneq  37728  cover2  38036  upixp  38050  indexdom  38055  filbcmb  38061  mettrifi  38078  mpobi123f  38483  rsp3  38687  riotasvd  39402  glbconxN  39824  cdlemefr29exN  40848  cdlemk36  41359  aks4d1p7d1  42521  mptfcl  43152  aomclem2  43483  hbtlem5  43556  gneispace  44561  trintALTVD  45306  trintALT  45307  modelaxrep  45408  refsumcn  45461  rfcnnnub  45467  choicefi  45629  mullimc  46046  mullimcf  46053  addlimc  46076  itgsubsticclem  46403  stoweidlem25  46453  stoweidlem52  46480  stoweidlem59  46487  stoweidlem62  46490  wallispilem3  46495  stirlinglem13  46514  fourierdlem73  46607  natlocalincr  47306  ffnafv  47619  iunord  50151  setrec1lem2  50163