Theorem rsp 2913

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1473   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-ral 2901

This theorem is referenced by:  rspa  2914  rspec  2915  r19.21bi  2916  rsp2  2920  r19.12  3045  reupick2  3872  rspn0  3892  dfiun2g  4488  iinss2  4508  invdisj  4571  trssOLD  4690  reusv1  4792  reusv1OLD  4793  reusv2lem1  4794  reusv2lem3  4797  reusv3  4802  ralxfrALT  4813  fvmptss  6201  ffnfv  6295  riota5f  6535  mpt2eq123  6612  peano5  6981  fun11iun  7019  wfrlem4  7305  wfrlem12  7313  tfr3  7382  tz7.48-1  7425  tz7.49  7427  nneneq  8028  scottex  8631  dfac2  8836  infpssrlem4  9011  fin23lem30  9047  fin23lem31  9048  hsmexlem2  9132  domtriomlem  9147  axdc3lem2  9156  axdc3lem4  9158  konigthlem  9269  winalim2  9397  nqereu  9630  dedekind  10079  dedekindle  10080  prodeq2ii  14482  vdwlem9  15531  mreiincl  16079  srgi  18334  ringi  18383  lbsextlem3  18981  lbsextlem4  18982  tgcl  20584  txindis  21247  alexsubALTlem3  21663  prdsxmslem2  22144  fsumcn  22481  lebnumlem1  22568  iscmet3lem1  22897  iscmet3lem2  22898  ovoliunlem2  23078  mbfimaopnlem  23228  limciun  23464  ftalem3  24601  ostth3  25127  mptelee  25575  ubthlem2  27111  aciunf1lem  28844  esumcvg  29475  bnj228  30057  bnj590  30234  bnj594  30236  bnj600  30243  bnj1128  30312  bnj1125  30314  bnj1145  30315  bnj1398  30356  bnj1417  30363  dfon2lem3  30934  dfon2lem7  30938  trpredmintr  30975  frr3g  31023  frrlem4  31027  frrlem11  31036  neibastop1  31524  unblimceq0lem  31667  unbdqndv2  31672  cover2  32678  upixp  32694  indexdom  32699  filbcmb  32705  mettrifi  32723  mpt2bi123f  33141  riotasvd  33260  glbconxN  33682  cdlemefr29exN  34708  cdlemk36  35219  mptfcl  36301  aomclem2  36643  hbtlem5  36717  gneispace  37452  trintALTVD  38138  trintALT  38139  refsumcn  38212  rfcnnnub  38218  choicefi  38387  mullimc  38683  mullimcf  38690  addlimc  38715  itgsubsticclem  38867  stoweidlem25  38918  stoweidlem52  38945  stoweidlem59  38952  stoweidlem62  38955  wallispilem3  38960  stirlinglem13  38979  fourierdlem73  39072  2reu1  39835  ffnafv  39900  iunord  42220  setrec1lem2  42234