Theorem rsp 3250

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1558   ∈ wcel 2142  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-ex 1800  df-ral 3077

This theorem is referenced by:  rspa  3251  rspec  3253  rsp2  3279  r19.12  3311  2reu1  3850  reupick2  4283  iuneqconst  4961  iinss2  5015  invdisj  5086  reusv1  5354  reusv2lem1  5355  reusv2lem3  5357  reusv3  5362  ralxfrALT  5372  fvmptss  6988  ffnfv  7100  riota5f  7381  mpoeq123  7468  frrlem4  8270  frrlem8  8274  frrlem10  8276  frrlem13  8279  tfr3  8370  tz7.48-1  8414  tz7.49  8416  nneneq  9174  frr3g  9714  scottex  9843  dfac2b  10087  infpssrlem4  10263  fin23lem30  10299  fin23lem31  10300  hsmexlem2  10384  domtriomlem  10399  axdc3lem2  10408  axdc3lem4  10410  konigthlem  10526  winalim2  10654  nqereu  10887  dedekind  11346  dedekindle  11347  prodeq2ii  15941  vdwlem9  17025  mreiincl  17624  sgrpidmnd  18773  srgdilem  20238  ringdilem  20295  lbsextlem3  21227  lbsextlem4  21228  tgcl  23026  txindis  23691  alexsubALTlem3  24106  prdsxmslem2  24586  fsumcn  24929  lebnumlem1  25020  iscmet3lem1  25350  iscmet3lem2  25351  ovoliunlem2  25562  mbfimaopnlem  25714  limciun  25953  ftalem3  27136  ostth3  27699  precsexlem10  28306  precsexlem11  28307  z12zsodd  28572  mpteleeOLD  29093  ubthlem2  31071  aciunf1lem  32861  esumcvg  34380  bnj228  35028  bnj590  35202  bnj594  35204  bnj600  35211  bnj1128  35282  bnj1125  35284  bnj1145  35285  bnj1398  35326  bnj1417  35333  dfon2lem3  36130  dfon2lem7  36134  neibastop1  36716  weiunlem  36820  unblimceq0lem  36941  unbdqndv2  36946  rdgssun  37869  ralssiun  37898  fvineqsneu  37902  fvineqsneq  37903  cover2  38211  upixp  38225  indexdom  38230  filbcmb  38236  mettrifi  38253  mpobi123f  38658  rsp3  38862  riotasvd  39577  glbconxN  39999  cdlemefr29exN  41023  cdlemk36  41534  aks4d1p7d1  42696  mptfcl  43298  aomclem2  43629  hbtlem5  43702  gneispace  44707  trintALTVD  45452  trintALT  45453  modelaxrep  45554  refsumcn  45607  rfcnnnub  45613  choicefi  45774  mullimc  46189  mullimcf  46196  addlimc  46219  itgsubsticclem  46546  stoweidlem25  46596  stoweidlem52  46623  stoweidlem59  46630  stoweidlem62  46633  wallispilem3  46638  stirlinglem13  46657  fourierdlem73  46750  natlocalincr  47449  ffnafv  47762  iunord  50294  setrec1lem2  50306