Theorem rsp 3240

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1532   ∈ wcel 2099  ∀wral 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2167

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-ral 3058

This theorem is referenced by:  rspa  3241  rspec  3243  rsp2  3270  r19.12  3307  r19.12OLD  3308  2reu1  3888  reupick2  4316  rspn0OLD  4349  iuneqconst  5002  iinss2  5054  invdisj  5126  reusv1  5391  reusv2lem1  5392  reusv2lem3  5394  reusv3  5399  ralxfrALT  5409  fvmptss  7011  ffnfv  7123  riota5f  7399  mpoeq123  7486  peano5OLD  7894  frrlem4  8288  frrlem8  8292  frrlem10  8294  frrlem13  8297  wfrlem4OLD  8326  wfrlem12OLD  8334  tfr3  8413  tz7.48-1  8457  tz7.49  8459  nneneq  9227  nneneqOLD  9239  frr3g  9773  scottex  9902  dfac2b  10147  infpssrlem4  10323  fin23lem30  10359  fin23lem31  10360  hsmexlem2  10444  domtriomlem  10459  axdc3lem2  10468  axdc3lem4  10470  konigthlem  10585  winalim2  10713  nqereu  10946  dedekind  11401  dedekindle  11402  prodeq2ii  15883  vdwlem9  16951  mreiincl  17569  sgrpidmnd  18692  srgdilem  20125  ringdilem  20182  lbsextlem3  21041  lbsextlem4  21042  tgcl  22865  txindis  23531  alexsubALTlem3  23946  prdsxmslem2  24431  fsumcn  24781  lebnumlem1  24880  iscmet3lem1  25212  iscmet3lem2  25213  ovoliunlem2  25425  mbfimaopnlem  25577  limciun  25816  ftalem3  27000  ostth3  27564  precsexlem10  28107  precsexlem11  28108  mptelee  28699  ubthlem2  30674  aciunf1lem  32441  esumcvg  33699  bnj228  34360  bnj590  34535  bnj594  34537  bnj600  34544  bnj1128  34615  bnj1125  34617  bnj1145  34618  bnj1398  34659  bnj1417  34666  dfon2lem3  35375  dfon2lem7  35379  neibastop1  35837  unblimceq0lem  35975  unbdqndv2  35980  rdgssun  36851  ralssiun  36880  fvineqsneu  36884  fvineqsneq  36885  cover2  37182  upixp  37196  indexdom  37201  filbcmb  37207  mettrifi  37224  mpobi123f  37629  riotasvd  38422  glbconxN  38845  cdlemefr29exN  39869  cdlemk36  40380  aks4d1p7d1  41547  mptfcl  42134  aomclem2  42473  hbtlem5  42546  gneispace  43558  trintALTVD  44313  trintALT  44314  refsumcn  44386  rfcnnnub  44392  choicefi  44567  mullimc  44998  mullimcf  45005  addlimc  45030  itgsubsticclem  45357  stoweidlem25  45407  stoweidlem52  45434  stoweidlem59  45441  stoweidlem62  45444  wallispilem3  45449  stirlinglem13  45468  fourierdlem73  45561  natlocalincr  46256  ffnafv  46545  iunord  48101  setrec1lem2  48113