Theorem rsp 3253

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1568   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-ral 3080

This theorem is referenced by:  rspa  3254  rspec  3256  rsp2  3282  r19.12  3314  2reu1  3851  reupick2  4284  iuneqconst  4968  iinss2  5022  invdisj  5095  reusv1  5368  reusv2lem1  5369  reusv2lem3  5371  reusv3  5376  ralxfrALT  5386  fvmptss  7002  ffnfv  7114  riota5f  7395  mpoeq123  7482  frrlem4  8282  frrlem8  8286  frrlem10  8288  frrlem13  8291  tfr3  8382  tz7.48-1  8426  tz7.49  8428  nneneq  9186  frr3g  9724  scottex  9855  dfac2b  10110  infpssrlem4  10285  fin23lem30  10321  fin23lem31  10322  hsmexlem2  10406  domtriomlem  10421  axdc3lem2  10430  axdc3lem4  10432  konigthlem  10548  winalim2  10676  nqereu  10909  dedekind  11368  dedekindle  11369  prodeq2ii  15961  vdwlem9  17044  mreiincl  17643  sgrpidmnd  18792  srgdilem  20269  ringdilem  20326  lbsextlem3  21284  lbsextlem4  21285  tgcl  23126  txindis  23791  alexsubALTlem3  24206  prdsxmslem2  24686  fsumcn  25029  lebnumlem1  25120  iscmet3lem1  25450  iscmet3lem2  25451  ovoliunlem2  25662  mbfimaopnlem  25814  limciun  26053  ftalem3  27239  ostth3  27802  precsexlem10  28409  precsexlem11  28410  z12zsodd  28675  mpteleeOLD  29245  ubthlem2  31223  aciunf1lem  33007  esumcvg  34476  bnj228  35124  bnj590  35298  bnj594  35300  bnj600  35307  bnj1128  35378  bnj1125  35380  bnj1145  35381  bnj1398  35422  bnj1417  35429  dfon2lem3  36275  dfon2lem7  36279  neibastop1  36870  weiunlem  36974  unblimceq0lem  37095  unbdqndv2  37100  rdgssun  38024  ralssiun  38053  fvineqsneu  38057  fvineqsneq  38058  cover2  38366  upixp  38380  indexdom  38385  filbcmb  38391  mettrifi  38408  mpobi123f  38811  rsp3  39015  riotasvd  39730  glbconxN  40152  cdlemefr29exN  41176  cdlemk36  41687  aks4d1p7d1  42849  mptfcl  43451  aomclem2  43782  hbtlem5  43855  gneispace  44860  trintALTVD  45588  trintALT  45589  modelaxrep  45690  refsumcn  45750  rfcnnnub  45756  choicefi  45917  mullimc  46332  mullimcf  46339  addlimc  46362  itgsubsticclem  46689  stoweidlem25  46739  stoweidlem52  46766  stoweidlem59  46773  stoweidlem62  46776  wallispilem3  46781  stirlinglem13  46800  fourierdlem73  46893  natlocalincr  47592  ffnafv  47908  iunord  50454  setrec1lem2  50466