Theorem rsp 3243

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2106  ∀wral 3060

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-ral 3061

This theorem is referenced by:  rspa  3244  rspec  3246  rsp2  3273  r19.12  3310  r19.12OLD  3311  2reu1  3887  reupick2  4316  rspn0OLD  4349  iuneqconst  5001  iinss2  5053  invdisj  5125  reusv1  5388  reusv2lem1  5389  reusv2lem3  5391  reusv3  5396  ralxfrALT  5406  fvmptss  6996  ffnfv  7102  riota5f  7378  mpoeq123  7465  peano5OLD  7867  frrlem4  8256  frrlem8  8260  frrlem10  8262  frrlem13  8265  wfrlem4OLD  8294  wfrlem12OLD  8302  tfr3  8381  tz7.48-1  8425  tz7.49  8427  nneneq  9192  nneneqOLD  9204  frr3g  9733  scottex  9862  dfac2b  10107  infpssrlem4  10283  fin23lem30  10319  fin23lem31  10320  hsmexlem2  10404  domtriomlem  10419  axdc3lem2  10428  axdc3lem4  10430  konigthlem  10545  winalim2  10673  nqereu  10906  dedekind  11359  dedekindle  11360  prodeq2ii  15839  vdwlem9  16904  mreiincl  17522  sgrpidmnd  18607  srgdilem  19973  ringdilem  20030  lbsextlem3  20722  lbsextlem4  20723  tgcl  22401  txindis  23067  alexsubALTlem3  23482  prdsxmslem2  23967  fsumcn  24315  lebnumlem1  24406  iscmet3lem1  24737  iscmet3lem2  24738  ovoliunlem2  24949  mbfimaopnlem  25101  limciun  25340  ftalem3  26506  ostth3  27068  mptelee  28018  ubthlem2  29987  aciunf1lem  31756  esumcvg  32913  bnj228  33575  bnj590  33750  bnj594  33752  bnj600  33759  bnj1128  33830  bnj1125  33832  bnj1145  33833  bnj1398  33874  bnj1417  33881  dfon2lem3  34585  dfon2lem7  34589  neibastop1  35046  unblimceq0lem  35184  unbdqndv2  35189  rdgssun  36061  ralssiun  36090  fvineqsneu  36094  fvineqsneq  36095  cover2  36385  upixp  36400  indexdom  36405  filbcmb  36411  mettrifi  36428  mpobi123f  36833  riotasvd  37629  glbconxN  38052  cdlemefr29exN  39076  cdlemk36  39587  aks4d1p7d1  40750  mptfcl  41227  aomclem2  41566  hbtlem5  41639  gneispace  42654  trintALTVD  43410  trintALT  43411  refsumcn  43483  rfcnnnub  43489  choicefi  43668  mullimc  44103  mullimcf  44110  addlimc  44135  itgsubsticclem  44462  stoweidlem25  44512  stoweidlem52  44539  stoweidlem59  44546  stoweidlem62  44549  wallispilem3  44554  stirlinglem13  44573  fourierdlem73  44666  natlocalincr  45361  ffnafv  45649  iunord  47367  setrec1lem2  47379