Theorem rsp 3117

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1541   ∈ wcel 2112  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-12 2177

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-ral 3056

This theorem is referenced by:  rspa  3118  rspec  3119  rsp2  3124  r19.12  3233  2reu1  3796  reupick2  4221  rspn0OLD  4254  iuneqconst  4901  iinss2  4952  invdisj  5023  reusv1  5275  reusv2lem1  5276  reusv2lem3  5278  reusv3  5283  ralxfrALT  5293  fvmptss  6808  ffnfv  6913  riota5f  7177  mpoeq123  7261  peano5OLD  7650  frrlem4  8008  frrlem8  8012  frrlem10  8014  frrlem13  8017  wfrlem4  8036  wfrlem12  8044  tfr3  8113  tz7.48-1  8157  tz7.49  8159  nneneq  8807  trpredmintr  9314  scottex  9466  dfac2b  9709  infpssrlem4  9885  fin23lem30  9921  fin23lem31  9922  hsmexlem2  10006  domtriomlem  10021  axdc3lem2  10030  axdc3lem4  10032  konigthlem  10147  winalim2  10275  nqereu  10508  dedekind  10960  dedekindle  10961  prodeq2ii  15438  vdwlem9  16505  mreiincl  17053  sgrpidmnd  18132  srgi  19480  ringi  19532  lbsextlem3  20151  lbsextlem4  20152  tgcl  21820  txindis  22485  alexsubALTlem3  22900  prdsxmslem2  23381  fsumcn  23721  lebnumlem1  23812  iscmet3lem1  24142  iscmet3lem2  24143  ovoliunlem2  24354  mbfimaopnlem  24506  limciun  24745  ftalem3  25911  ostth3  26473  mptelee  26940  ubthlem2  28906  aciunf1lem  30673  esumcvg  31720  bnj228  32380  bnj590  32557  bnj594  32559  bnj600  32566  bnj1128  32637  bnj1125  32639  bnj1145  32640  bnj1398  32681  bnj1417  32688  dfon2lem3  33431  dfon2lem7  33435  frr3g  33504  neibastop1  34234  unblimceq0lem  34372  unbdqndv2  34377  rdgssun  35235  ralssiun  35264  fvineqsneu  35268  fvineqsneq  35269  cover2  35558  upixp  35573  indexdom  35578  filbcmb  35584  mettrifi  35601  mpobi123f  36006  riotasvd  36656  glbconxN  37078  cdlemefr29exN  38102  cdlemk36  38613  mptfcl  40186  aomclem2  40524  hbtlem5  40597  gneispace  41362  trintALTVD  42114  trintALT  42115  refsumcn  42187  rfcnnnub  42193  choicefi  42354  mullimc  42775  mullimcf  42782  addlimc  42807  itgsubsticclem  43134  stoweidlem25  43184  stoweidlem52  43211  stoweidlem59  43218  stoweidlem62  43221  wallispilem3  43226  stirlinglem13  43245  fourierdlem73  43338  ffnafv  44278  iunord  45996  setrec1lem2  46008