Theorem rsp 3255

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

Assertion

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

Proof of Theorem rsp

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

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

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 1943  ax-6 2000  ax-7 2041  ax-12 2216

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

This theorem is used by:  rspa  3256  rspec  3258  rsp2  3284  r19.12  3316  2reu1  3852  reupick2  4284  iuneqconst  4970  iinss2  5024  invdisj  5097  reusv1  5370  reusv2lem1  5371  reusv2lem3  5373  reusv3  5378  ralxfrALT  5388  fvmptss  7006  ffnfv  7118  riota5f  7404  mpoeq123  7491  frrlem4  8292  frrlem8  8296  frrlem10  8298  frrlem13  8301  tfr3  8392  tz7.48-1  8436  tz7.49  8438  nneneq  9197  frr3g  9735  scottexOLD  9870  dfac2b  10130  infpssrlem4  10305  fin23lem30  10341  fin23lem31  10342  hsmexlem2  10426  domtriomlem  10441  axdc3lem2  10450  axdc3lem4  10452  konigthlem  10568  winalim2  10696  nqereu  10929  dedekind  11388  dedekindle  11389  prodeq2ii  15988  vdwlem9  17071  mreiincl  17670  sgrpidmnd  18829  srgdilem  20318  ringdilem  20375  lbsextlem3  21334  lbsextlem4  21335  tgcl  23176  txindis  23842  alexsubALTlem3  24257  prdsxmslem2  24737  fsumcn  25080  lebnumlem1  25171  iscmet3lem1  25501  iscmet3lem2  25502  ovoliunlem2  25713  mbfimaopnlem  25865  limciun  26104  ftalem3  27290  ostth3  27853  precsexlem10  28460  precsexlem11  28461  z12zsodd  28726  mpteleeOLD  29300  ubthlem2  31294  aciunf1lem  33078  esumcvg  34540  bnj228  35189  bnj590  35363  bnj594  35365  bnj600  35372  bnj1128  35443  bnj1125  35445  bnj1145  35446  bnj1398  35487  bnj1417  35494  dfon2lem3  36312  dfon2lem7  36316  neibastop1  36927  weiunlem  37031  unblimceq0lem  37152  unbdqndv2  37157  rdgssun  38081  ralssiun  38110  fvineqsneu  38114  fvineqsneq  38115  cover2  38424  upixp  38438  indexdom  38443  filbcmb  38449  mettrifi  38466  mpobi123f  38869  rsp3  39073  riotasvd  39788  glbconxN  40210  cdlemefr29exN  41234  cdlemk36  41745  aks4d1p7d1  42907  mptfcl  43509  aomclem2  43840  hbtlem5  43913  gneispace  44918  trintALTVD  45646  trintALT  45647  modelaxrep  45748  refsumcn  45808  rfcnnnub  45814  choicefi  45975  mullimc  46390  mullimcf  46397  addlimc  46420  itgsubsticclem  46747  stoweidlem25  46797  stoweidlem52  46824  stoweidlem59  46831  stoweidlem62  46834  wallispilem3  46839  stirlinglem13  46858  fourierdlem73  46951  natlocalincr  47650  ffnafv  47966  iunord  50511  setrec1lem2  50523