Theorem rsp 3217

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  3218  rspec  3220  rsp2  3246  r19.12  3278  2reu1  3849  reupick2  4282  iuneqconst  4953  iinss2  5006  invdisj  5078  reusv1  5336  reusv2lem1  5337  reusv2lem3  5339  reusv3  5344  ralxfrALT  5354  fvmptss  6942  ffnfv  7053  riota5f  7334  mpoeq123  7421  frrlem4  8222  frrlem8  8226  frrlem10  8228  frrlem13  8231  tfr3  8321  tz7.48-1  8365  tz7.49  8367  nneneq  9120  frr3g  9652  scottex  9781  dfac2b  10025  infpssrlem4  10200  fin23lem30  10236  fin23lem31  10237  hsmexlem2  10321  domtriomlem  10336  axdc3lem2  10345  axdc3lem4  10347  konigthlem  10462  winalim2  10590  nqereu  10823  dedekind  11279  dedekindle  11280  prodeq2ii  15818  vdwlem9  16901  mreiincl  17498  sgrpidmnd  18613  srgdilem  20077  ringdilem  20134  lbsextlem3  21067  lbsextlem4  21068  tgcl  22854  txindis  23519  alexsubALTlem3  23934  prdsxmslem2  24415  fsumcn  24759  lebnumlem1  24858  iscmet3lem1  25189  iscmet3lem2  25190  ovoliunlem2  25402  mbfimaopnlem  25554  limciun  25793  ftalem3  26983  ostth3  27547  precsexlem10  28123  precsexlem11  28124  zs12zodd  28359  mptelee  28840  ubthlem2  30815  aciunf1lem  32605  esumcvg  34053  bnj228  34702  bnj590  34877  bnj594  34879  bnj600  34886  bnj1128  34957  bnj1125  34959  bnj1145  34960  bnj1398  35001  bnj1417  35008  dfon2lem3  35759  dfon2lem7  35763  neibastop1  36333  weiunlem2  36437  unblimceq0lem  36480  unbdqndv2  36485  rdgssun  37352  ralssiun  37381  fvineqsneu  37385  fvineqsneq  37386  cover2  37695  upixp  37709  indexdom  37714  filbcmb  37720  mettrifi  37737  mpobi123f  38142  riotasvd  38935  glbconxN  39357  cdlemefr29exN  40381  cdlemk36  40892  aks4d1p7d1  42055  mptfcl  42693  aomclem2  43028  hbtlem5  43101  gneispace  44107  trintALTVD  44853  trintALT  44854  modelaxrep  44955  refsumcn  45008  rfcnnnub  45014  choicefi  45178  mullimc  45597  mullimcf  45604  addlimc  45629  itgsubsticclem  45956  stoweidlem25  46006  stoweidlem52  46033  stoweidlem59  46040  stoweidlem62  46043  wallispilem3  46048  stirlinglem13  46067  fourierdlem73  46160  natlocalincr  46857  ffnafv  47155  iunord  49661  setrec1lem2  49673