Theorem rsp 3259

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1565   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-ral 3086

This theorem is referenced by:  rspa  3260  rspec  3262  rsp2  3288  r19.12  3320  2reu1  3859  reupick2  4292  iuneqconst  4972  iinss2  5026  invdisj  5099  reusv1  5369  reusv2lem1  5370  reusv2lem3  5372  reusv3  5377  ralxfrALT  5387  fvmptss  7003  ffnfv  7115  riota5f  7396  mpoeq123  7483  frrlem4  8285  frrlem8  8289  frrlem10  8291  frrlem13  8294  tfr3  8385  tz7.48-1  8429  tz7.49  8431  nneneq  9189  frr3g  9727  scottex  9858  dfac2b  10113  infpssrlem4  10289  fin23lem30  10325  fin23lem31  10326  hsmexlem2  10410  domtriomlem  10425  axdc3lem2  10434  axdc3lem4  10436  konigthlem  10552  winalim2  10680  nqereu  10913  dedekind  11372  dedekindle  11373  prodeq2ii  15964  vdwlem9  17048  mreiincl  17647  sgrpidmnd  18796  srgdilem  20273  ringdilem  20330  lbsextlem3  21261  lbsextlem4  21262  tgcl  23094  txindis  23759  alexsubALTlem3  24174  prdsxmslem2  24654  fsumcn  24997  lebnumlem1  25088  iscmet3lem1  25418  iscmet3lem2  25419  ovoliunlem2  25630  mbfimaopnlem  25782  limciun  26021  ftalem3  27204  ostth3  27767  precsexlem10  28374  precsexlem11  28375  z12zsodd  28640  mpteleeOLD  29185  ubthlem2  31163  aciunf1lem  32947  esumcvg  34420  bnj228  35068  bnj590  35242  bnj594  35244  bnj600  35251  bnj1128  35322  bnj1125  35324  bnj1145  35325  bnj1398  35366  bnj1417  35373  dfon2lem3  36173  dfon2lem7  36177  neibastop1  36758  weiunlem  36862  unblimceq0lem  36983  unbdqndv2  36988  rdgssun  37911  ralssiun  37940  fvineqsneu  37944  fvineqsneq  37945  cover2  38253  upixp  38267  indexdom  38272  filbcmb  38278  mettrifi  38295  mpobi123f  38700  rsp3  38904  riotasvd  39619  glbconxN  40041  cdlemefr29exN  41065  cdlemk36  41576  aks4d1p7d1  42738  mptfcl  43342  aomclem2  43673  hbtlem5  43746  gneispace  44751  trintALTVD  45479  trintALT  45480  modelaxrep  45581  refsumcn  45641  rfcnnnub  45647  choicefi  45808  mullimc  46223  mullimcf  46230  addlimc  46253  itgsubsticclem  46580  stoweidlem25  46630  stoweidlem52  46657  stoweidlem59  46664  stoweidlem62  46667  wallispilem3  46672  stirlinglem13  46691  fourierdlem73  46784  natlocalincr  47483  ffnafv  47796  iunord  50338  setrec1lem2  50350