Theorem rsp 3251

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

Assertion

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

Proof of Theorem rsp

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-ral 3078

This theorem is used by:  rspa  3252  rspec  3254  rsp2  3280  r19.12  3312  2reu1  3845  reupick2  4277  iuneqconst  4963  iinss2  5016  invdisj  5089  reusv1  5359  reusv2lem1  5360  reusv2lem3  5362  reusv3  5367  ralxfrALT  5377  fvmptss  7004  ffnfv  7117  riota5f  7403  mpoeq123  7490  frrlem4  8300  frrlem8  8304  frrlem10  8306  frrlem13  8309  tfr3  8400  tz7.48-1  8446  tz7.49  8448  nneneq  9214  frr3g  9753  scottexOLD  9927  setrec1lem2  9960  dfac2b  10202  infpssrlem4  10377  fin23lem30  10413  fin23lem31  10414  hsmexlem2  10498  domtriomlem  10513  axdc3lem2  10522  axdc3lem4  10524  konigthlem  10646  winalim2  10774  nqereu  11007  dedekind  11466  dedekindle  11467  prodeq2ii  16073  vdwlem9  17160  mreiincl  17759  sgrpidmnd  18921  srgdilem  20411  ringdilem  20469  lbsextlem3  21431  lbsextlem4  21432  tgcl  23280  txindis  23946  alexsubALTlem3  24361  prdsxmslem2  24841  fsumcn  25184  lebnumlem1  25275  iscmet3lem1  25605  iscmet3lem2  25606  ovoliunlem2  25817  mbfimaopnlem  25969  limciun  26207  ftalem3  27395  ostth3  27958  precsexlem10  28595  precsexlem11  28596  z12zsodd  28861  mpteleeOLD  29466  ubthlem2  31466  aciunf1lem  33249  esumcvg  34711  bnj228  35359  bnj590  35533  bnj594  35535  bnj600  35542  bnj1128  35613  bnj1125  35615  bnj1145  35616  bnj1398  35657  bnj1417  35664  dfon2lem3  36527  dfon2lem7  36531  neibastop1  37127  weiunlem  37231  mh-inf3f1  37309  unblimceq0lem  37352  unbdqndv2  37357  rdgssun  38281  ralssiun  38310  fvineqsneu  38314  fvineqsneq  38315  cover2  38629  upixp  38643  indexdom  38648  filbcmb  38654  mettrifi  38671  mpobi123f  39074  rsp3  39278  riotasvd  39993  glbconxN  40415  cdlemefr29exN  41439  cdlemk36  41950  aks4d1p7d1  43112  mptfcl  43710  aomclem2  44041  hbtlem5  44114  gneispace  45119  trintALTVD  45847  trintALT  45848  modelaxrep  45949  refsumcn  46016  rfcnnnub  46022  choicefi  46183  mullimc  46597  mullimcf  46604  addlimc  46627  itgsubsticclem  46954  stoweidlem25  47004  stoweidlem52  47031  stoweidlem59  47038  stoweidlem62  47041  wallispilem3  47046  stirlinglem13  47065  fourierdlem73  47158  ffnafv  48210  iunord  50753