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 2219	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑))
3	1, 2	sylbi 220	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-ral 3077

This theorem is used by:  rspa  3251  rspec  3253  rsp2  3279  r19.12  3311  2reu1  3844  reupick2  4276  iuneqconst  4962  iinss2  5015  invdisj  5088  reusv1  5358  reusv2lem1  5359  reusv2lem3  5361  reusv3  5366  ralxfrALT  5376  fvmptss  7006  ffnfv  7119  riota5f  7405  mpoeq123  7492  frrlem4  8307  frrlem8  8311  frrlem10  8313  frrlem13  8316  tfr3  8407  tz7.48-1  8453  tz7.49  8455  nneneq  9221  frr3g  9760  scottexOLD  9934  setrec1lem2  9967  dfac2b  10209  infpssrlem4  10384  fin23lem30  10420  fin23lem31  10421  hsmexlem2  10505  domtriomlem  10520  axdc3lem2  10529  axdc3lem4  10531  konigthlem  10653  winalim2  10781  nqereu  11014  dedekind  11473  dedekindle  11474  prodeq2ii  16080  vdwlem9  17167  mreiincl  17766  sgrpidmnd  18928  srgdilem  20418  ringdilem  20476  lbsextlem3  21438  lbsextlem4  21439  tgcl  23287  txindis  23953  alexsubALTlem3  24368  prdsxmslem2  24848  fsumcn  25191  lebnumlem1  25282  iscmet3lem1  25612  iscmet3lem2  25613  ovoliunlem2  25824  mbfimaopnlem  25976  limciun  26214  ftalem3  27402  ostth3  27965  precsexlem10  28602  precsexlem11  28603  z12zsodd  28868  mpteleeOLD  29473  ubthlem2  31473  aciunf1lem  33298  esumcvg  34760  bnj228  35408  bnj590  35582  bnj594  35584  bnj600  35591  bnj1128  35662  bnj1125  35664  bnj1145  35665  bnj1398  35706  bnj1417  35713  dfon2lem3  36589  dfon2lem7  36593  neibastop1  37189  weiunlem  37293  mh-inf3f1  37371  unblimceq0lem  37414  unbdqndv2  37419  rdgssun  38344  ralssiun  38373  fvineqsneu  38377  fvineqsneq  38378  cover2  38692  upixp  38706  indexdom  38711  filbcmb  38717  mettrifi  38734  mpobi123f  39137  rsp3  39341  riotasvd  40056  glbconxN  40478  cdlemefr29exN  41502  cdlemk36  42013  aks4d1p7d1  43175  mptfcl  43773  aomclem2  44099  hbtlem5  44172  gneispace  45176  trintALTVD  45904  trintALT  45905  modelaxrep  46013  refsumcn  46089  rfcnnnub  46095  choicefi  46256  mullimc  46670  mullimcf  46677  addlimc  46700  itgsubsticclem  47027  stoweidlem25  47077  stoweidlem52  47104  stoweidlem59  47111  stoweidlem62  47114  wallispilem3  47119  stirlinglem13  47138  fourierdlem73  47231  ffnafv  48283  iunord  50826