Theorem rsp 3111

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1599   ∈ wcel 2107  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-12 2163

This theorem depends on definitions:  df-bi 199  df-ex 1824  df-ral 3095

This theorem is referenced by:  rspa  3112  rspec  3113  r19.21bi  3114  rsp2  3118  r19.12  3248  r19.12OLD  3249  reupick2  4139  rspn0  4162  dfiun2g  4787  iinss2  4807  invdisj  4874  reusv1  5111  reusv2lem1  5112  reusv2lem3  5114  reusv3  5119  ralxfrALT  5129  fvmptss  6555  ffnfv  6654  riota5f  6910  mpt2eq123  6993  peano5  7369  fun11iun  7407  wfrlem4  7702  wfrlem4OLD  7703  wfrlem12  7711  tfr3  7780  tz7.48-1  7823  tz7.49  7825  nneneq  8433  scottex  9047  dfac2b  9288  dfac2OLD  9290  infpssrlem4  9465  fin23lem30  9501  fin23lem31  9502  hsmexlem2  9586  domtriomlem  9601  axdc3lem2  9610  axdc3lem4  9612  konigthlem  9727  winalim2  9855  nqereu  10088  dedekind  10541  dedekindle  10542  prodeq2ii  15055  vdwlem9  16108  mreiincl  16653  srgi  18909  ringi  18958  lbsextlem3  19568  lbsextlem4  19569  tgcl  21192  txindis  21857  alexsubALTlem3  22272  prdsxmslem2  22753  fsumcn  23092  lebnumlem1  23179  iscmet3lem1  23508  iscmet3lem2  23509  ovoliunlem2  23718  mbfimaopnlem  23870  limciun  24106  ftalem3  25264  ostth3  25796  mptelee  26261  ubthlem2  28316  aciunf1lem  30044  esumcvg  30754  bnj228  31411  bnj590  31587  bnj594  31589  bnj600  31596  bnj1128  31665  bnj1125  31667  bnj1145  31668  bnj1398  31709  bnj1417  31716  dfon2lem3  32286  dfon2lem7  32290  trpredmintr  32327  frr3g  32376  frrlem4  32380  frrlem11  32389  sslttr  32511  neibastop1  32950  unblimceq0lem  33087  unbdqndv2  33092  cover2  34142  upixp  34158  indexdom  34163  filbcmb  34169  mettrifi  34186  mpt2bi123f  34602  riotasvd  35119  glbconxN  35541  cdlemefr29exN  36565  cdlemk36  37076  mptfcl  38257  aomclem2  38598  hbtlem5  38671  gneispace  39402  trintALTVD  40063  trintALT  40064  refsumcn  40136  rfcnnnub  40142  choicefi  40327  mullimc  40770  mullimcf  40777  addlimc  40802  itgsubsticclem  41132  stoweidlem25  41183  stoweidlem52  41210  stoweidlem59  41217  stoweidlem62  41220  wallispilem3  41225  stirlinglem13  41244  fourierdlem73  41337  2reu1  42161  ffnafv  42226  iunord  43541  setrec1lem2  43554