Theorem rsp 3245

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-ral 3060

This theorem is referenced by:  rspa  3246  rspec  3248  rsp2  3275  r19.12  3312  r19.12OLD  3313  2reu1  3906  reupick2  4337  iuneqconst  5008  iinss2  5062  invdisj  5134  reusv1  5403  reusv2lem1  5404  reusv2lem3  5406  reusv3  5411  ralxfrALT  5421  fvmptss  7028  ffnfv  7139  riota5f  7416  mpoeq123  7505  frrlem4  8313  frrlem8  8317  frrlem10  8319  frrlem13  8322  wfrlem4OLD  8351  wfrlem12OLD  8359  tfr3  8438  tz7.48-1  8482  tz7.49  8484  nneneq  9244  nneneqOLD  9256  frr3g  9794  scottex  9923  dfac2b  10169  infpssrlem4  10344  fin23lem30  10380  fin23lem31  10381  hsmexlem2  10465  domtriomlem  10480  axdc3lem2  10489  axdc3lem4  10491  konigthlem  10606  winalim2  10734  nqereu  10967  dedekind  11422  dedekindle  11423  prodeq2ii  15944  vdwlem9  17023  mreiincl  17641  sgrpidmnd  18765  srgdilem  20210  ringdilem  20267  lbsextlem3  21180  lbsextlem4  21181  tgcl  22992  txindis  23658  alexsubALTlem3  24073  prdsxmslem2  24558  fsumcn  24908  lebnumlem1  25007  iscmet3lem1  25339  iscmet3lem2  25340  ovoliunlem2  25552  mbfimaopnlem  25704  limciun  25944  ftalem3  27133  ostth3  27697  precsexlem10  28255  precsexlem11  28256  mptelee  28925  ubthlem2  30900  aciunf1lem  32679  esumcvg  34067  bnj228  34728  bnj590  34903  bnj594  34905  bnj600  34912  bnj1128  34983  bnj1125  34985  bnj1145  34986  bnj1398  35027  bnj1417  35034  dfon2lem3  35767  dfon2lem7  35771  neibastop1  36342  weiunlem2  36446  unblimceq0lem  36489  unbdqndv2  36494  rdgssun  37361  ralssiun  37390  fvineqsneu  37394  fvineqsneq  37395  cover2  37702  upixp  37716  indexdom  37721  filbcmb  37727  mettrifi  37744  mpobi123f  38149  riotasvd  38938  glbconxN  39361  cdlemefr29exN  40385  cdlemk36  40896  aks4d1p7d1  42064  mptfcl  42708  aomclem2  43044  hbtlem5  43117  gneispace  44124  trintALTVD  44878  trintALT  44879  modelaxrep  44946  refsumcn  44968  rfcnnnub  44974  choicefi  45143  mullimc  45572  mullimcf  45579  addlimc  45604  itgsubsticclem  45931  stoweidlem25  45981  stoweidlem52  46008  stoweidlem59  46015  stoweidlem62  46018  wallispilem3  46023  stirlinglem13  46042  fourierdlem73  46135  natlocalincr  46830  ffnafv  47121  iunord  48907  setrec1lem2  48919