Theorem rsp 3226

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-ral 3053

This theorem is referenced by:  rspa  3227  rspec  3229  rsp2  3255  r19.12  3287  2reu1  3849  reupick2  4285  iuneqconst  4960  iinss2  5015  invdisj  5086  reusv1  5344  reusv2lem1  5345  reusv2lem3  5347  reusv3  5352  ralxfrALT  5362  fvmptss  6962  ffnfv  7073  riota5f  7353  mpoeq123  7440  frrlem4  8241  frrlem8  8245  frrlem10  8247  frrlem13  8250  tfr3  8340  tz7.48-1  8384  tz7.49  8386  nneneq  9142  frr3g  9680  scottex  9809  dfac2b  10053  infpssrlem4  10228  fin23lem30  10264  fin23lem31  10265  hsmexlem2  10349  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  konigthlem  10491  winalim2  10619  nqereu  10852  dedekind  11308  dedekindle  11309  prodeq2ii  15846  vdwlem9  16929  mreiincl  17527  sgrpidmnd  18676  srgdilem  20139  ringdilem  20196  lbsextlem3  21127  lbsextlem4  21128  tgcl  22925  txindis  23590  alexsubALTlem3  24005  prdsxmslem2  24485  fsumcn  24829  lebnumlem1  24928  iscmet3lem1  25259  iscmet3lem2  25260  ovoliunlem2  25472  mbfimaopnlem  25624  limciun  25863  ftalem3  27053  ostth3  27617  precsexlem10  28224  precsexlem11  28225  z12zsodd  28490  mpteleeOLD  28980  ubthlem2  30959  aciunf1lem  32752  esumcvg  34264  bnj228  34912  bnj590  35086  bnj594  35088  bnj600  35095  bnj1128  35166  bnj1125  35168  bnj1145  35169  bnj1398  35210  bnj1417  35217  dfon2lem3  35999  dfon2lem7  36003  neibastop1  36575  weiunlem  36679  unblimceq0lem  36728  unbdqndv2  36733  rdgssun  37633  ralssiun  37662  fvineqsneu  37666  fvineqsneq  37667  cover2  37966  upixp  37980  indexdom  37985  filbcmb  37991  mettrifi  38008  mpobi123f  38413  rsp3  38617  riotasvd  39332  glbconxN  39754  cdlemefr29exN  40778  cdlemk36  41289  aks4d1p7d1  42452  mptfcl  43077  aomclem2  43412  hbtlem5  43485  gneispace  44490  trintALTVD  45235  trintALT  45236  modelaxrep  45337  refsumcn  45390  rfcnnnub  45396  choicefi  45558  mullimc  45976  mullimcf  45983  addlimc  46006  itgsubsticclem  46333  stoweidlem25  46383  stoweidlem52  46410  stoweidlem59  46417  stoweidlem62  46420  wallispilem3  46425  stirlinglem13  46444  fourierdlem73  46537  natlocalincr  47234  ffnafv  47531  iunord  50035  setrec1lem2  50047