Theorem rsp 3207

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2114  ∀wral 3140

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 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-ral 3145

This theorem is referenced by:  rspa  3208  rspec  3209  r19.21biOLD  3211  rsp2  3215  r19.12  3326  r19.12OLD  3329  2reu1  3883  reupick2  4291  rspn0  4315  iuneqconst  4932  dfiun2gOLD  4958  iinss2  4983  invdisj  5052  reusv1  5300  reusv2lem1  5301  reusv2lem3  5303  reusv3  5308  ralxfrALT  5318  fvmptss  6782  ffnfv  6884  riota5f  7144  mpoeq123  7228  peano5  7607  wfrlem4  7960  wfrlem12  7968  tfr3  8037  tz7.48-1  8081  tz7.49  8083  nneneq  8702  scottex  9316  dfac2b  9558  infpssrlem4  9730  fin23lem30  9766  fin23lem31  9767  hsmexlem2  9851  domtriomlem  9866  axdc3lem2  9875  axdc3lem4  9877  konigthlem  9992  winalim2  10120  nqereu  10353  dedekind  10805  dedekindle  10806  prodeq2ii  15269  vdwlem9  16327  mreiincl  16869  sgrpidmnd  17918  srgi  19263  ringi  19312  lbsextlem3  19934  lbsextlem4  19935  tgcl  21579  txindis  22244  alexsubALTlem3  22659  prdsxmslem2  23141  fsumcn  23480  lebnumlem1  23567  iscmet3lem1  23896  iscmet3lem2  23897  ovoliunlem2  24106  mbfimaopnlem  24258  limciun  24494  ftalem3  25654  ostth3  26216  mptelee  26683  ubthlem2  28650  aciunf1lem  30409  esumcvg  31347  bnj228  32007  bnj590  32184  bnj594  32186  bnj600  32193  bnj1128  32264  bnj1125  32266  bnj1145  32267  bnj1398  32308  bnj1417  32315  dfon2lem3  33032  dfon2lem7  33036  trpredmintr  33072  frr3g  33123  frrlem4  33128  frrlem8  33132  frrlem10  33134  frrlem13  33137  sslttr  33270  neibastop1  33709  unblimceq0lem  33847  unbdqndv2  33852  rdgssun  34661  ralssiun  34690  fvineqsneu  34694  fvineqsneq  34695  cover2  34991  upixp  35006  indexdom  35011  filbcmb  35017  mettrifi  35034  mpobi123f  35442  riotasvd  36094  glbconxN  36516  cdlemefr29exN  37540  cdlemk36  38051  mptfcl  39324  aomclem2  39662  hbtlem5  39735  gneispace  40491  trintALTVD  41221  trintALT  41222  refsumcn  41294  rfcnnnub  41300  choicefi  41470  mullimc  41904  mullimcf  41911  addlimc  41936  itgsubsticclem  42267  stoweidlem25  42317  stoweidlem52  42344  stoweidlem59  42351  stoweidlem62  42354  wallispilem3  42359  stirlinglem13  42378  fourierdlem73  42471  ffnafv  43377  iunord  44786  setrec1lem2  44798