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 1568   ∈ wcel 2145  ∀wral 3076

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 2213

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

This theorem is used by:  rspa  3251  rspec  3253  rsp2  3279  r19.12  3311  2reu1  3845  reupick2  4277  iuneqconst  4963  iinss2  5016  invdisj  5089  reusv1  5362  reusv2lem1  5363  reusv2lem3  5365  reusv3  5370  ralxfrALT  5380  fvmptss  6999  ffnfv  7112  riota5f  7398  mpoeq123  7485  frrlem4  8288  frrlem8  8292  frrlem10  8294  frrlem13  8297  tfr3  8388  tz7.48-1  8432  tz7.49  8434  nneneq  9200  frr3g  9738  scottexOLD  9873  dfac2b  10133  infpssrlem4  10308  fin23lem30  10344  fin23lem31  10345  hsmexlem2  10429  domtriomlem  10444  axdc3lem2  10453  axdc3lem4  10455  konigthlem  10577  winalim2  10705  nqereu  10938  dedekind  11397  dedekindle  11398  prodeq2ii  16000  vdwlem9  17081  mreiincl  17680  sgrpidmnd  18841  srgdilem  20331  ringdilem  20388  lbsextlem3  21347  lbsextlem4  21348  tgcl  23194  txindis  23860  alexsubALTlem3  24275  prdsxmslem2  24755  fsumcn  25098  lebnumlem1  25189  iscmet3lem1  25519  iscmet3lem2  25520  ovoliunlem2  25731  mbfimaopnlem  25883  limciun  26121  ftalem3  27311  ostth3  27874  precsexlem10  28481  precsexlem11  28482  z12zsodd  28747  mpteleeOLD  29352  ubthlem2  31352  aciunf1lem  33135  esumcvg  34596  bnj228  35245  bnj590  35419  bnj594  35421  bnj600  35428  bnj1128  35499  bnj1125  35501  bnj1145  35502  bnj1398  35543  bnj1417  35550  dfon2lem3  36362  dfon2lem7  36366  neibastop1  36978  weiunlem  37082  unblimceq0lem  37203  unbdqndv2  37208  rdgssun  38132  ralssiun  38161  fvineqsneu  38165  fvineqsneq  38166  cover2  38465  upixp  38479  indexdom  38484  filbcmb  38490  mettrifi  38507  mpobi123f  38910  rsp3  39114  riotasvd  39829  glbconxN  40251  cdlemefr29exN  41275  cdlemk36  41786  aks4d1p7d1  42948  mptfcl  43565  aomclem2  43896  hbtlem5  43969  gneispace  44974  trintALTVD  45702  trintALT  45703  modelaxrep  45804  refsumcn  45864  rfcnnnub  45870  choicefi  46031  mullimc  46446  mullimcf  46453  addlimc  46476  itgsubsticclem  46803  stoweidlem25  46853  stoweidlem52  46880  stoweidlem59  46887  stoweidlem62  46890  wallispilem3  46895  stirlinglem13  46914  fourierdlem73  47007  ffnafv  48059  iunord  50602  setrec1lem2  50614