Theorem rsp 3254

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

Assertion

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

Proof of Theorem rsp

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813  df-ral 3081

This theorem is used by:  rspa  3255  rspec  3257  rsp2  3283  r19.12  3315  2reu1  3849  reupick2  4279  iuneqconst  4968  iinss2  5021  invdisj  5094  reusv1  5366  reusv2lem1  5367  reusv2lem3  5369  reusv3  5374  ralxfrALT  5384  fvmptss  7037  ffnfv  7151  riota5f  7436  mpoeq123  7523  frrlem4  8345  frrlem8  8349  frrlem10  8351  frrlem13  8354  tfr3  8445  tz7.48-1  8491  tz7.49  8493  nneneq  9259  frr3g  9797  scottexOLD  9971  setrec1lem2  10004  dfac2b  10248  infpssrlem4  10423  fin23lem30  10459  fin23lem31  10460  hsmexlem2  10544  domtriomlem  10559  axdc3lem2  10568  axdc3lem4  10570  konigthlem  10692  winalim2  10820  nqereu  11053  dedekind  11512  dedekindle  11513  prodeq2ii  16124  vdwlem9  17211  mreiincl  17816  sgrpidmnd  18978  srgdilem  20469  ringdilem  20527  lbsextlem3  21489  lbsextlem4  21490  tgcl  23342  txindis  24008  alexsubALTlem3  24423  prdsxmslem2  24903  fsumcn  25246  lebnumlem1  25337  iscmet3lem1  25667  iscmet3lem2  25668  ovoliunlem2  25879  mbfimaopnlem  26031  limciun  26269  ftalem3  27459  ostth3  28022  precsexlem10  28659  precsexlem11  28660  z12zsodd  28925  mpteleeOLD  29530  ubthlem2  31530  aciunf1lem  33354  esumcvg  34829  bnj228  35477  bnj590  35651  bnj594  35653  bnj600  35660  bnj1128  35731  bnj1125  35733  bnj1145  35734  bnj1398  35775  bnj1417  35782  dfon2lem3  36762  dfon2lem7  36766  neibastop1  37362  weiunlem  37466  mh-inf3f1  37544  unblimceq0lem  37587  unbdqndv2  37592  rdgssun  38569  ralssiun  38598  fvineqsneu  38602  fvineqsneq  38603  cover2  38917  upixp  38931  indexdom  38936  filbcmb  38940  mettrifi  38957  mpobi123f  39360  rsp3  39564  riotasvd  40279  glbconxN  40701  cdlemefr29exN  41725  cdlemk36  42236  aks4d1p7d1  43398  mptfcl  43997  aomclem2  44323  hbtlem5  44395  gneispace  45395  trintALTVD  46122  trintALT  46123  modelaxrep  46235  refsumcn  46321  rfcnnnub  46327  choicefi  46487  mullimc  46901  mullimcf  46908  addlimc  46931  itgsubsticclem  47258  stoweidlem25  47308  stoweidlem52  47335  stoweidlem59  47342  stoweidlem62  47345  wallispilem3  47350  stirlinglem13  47369  fourierdlem73  47462  ffnafv  48514  iunord  51190