Theorem rsp 3225

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-ral 3045

This theorem is referenced by:  rspa  3226  rspec  3228  rsp2  3254  r19.12  3288  2reu1  3860  reupick2  4294  iuneqconst  4967  iinss2  5021  invdisj  5093  reusv1  5352  reusv2lem1  5353  reusv2lem3  5355  reusv3  5360  ralxfrALT  5370  fvmptss  6980  ffnfv  7091  riota5f  7372  mpoeq123  7461  frrlem4  8268  frrlem8  8272  frrlem10  8274  frrlem13  8277  tfr3  8367  tz7.48-1  8411  tz7.49  8413  nneneq  9170  frr3g  9709  scottex  9838  dfac2b  10084  infpssrlem4  10259  fin23lem30  10295  fin23lem31  10296  hsmexlem2  10380  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  konigthlem  10521  winalim2  10649  nqereu  10882  dedekind  11337  dedekindle  11338  prodeq2ii  15877  vdwlem9  16960  mreiincl  17557  sgrpidmnd  18666  srgdilem  20101  ringdilem  20158  lbsextlem3  21070  lbsextlem4  21071  tgcl  22856  txindis  23521  alexsubALTlem3  23936  prdsxmslem2  24417  fsumcn  24761  lebnumlem1  24860  iscmet3lem1  25191  iscmet3lem2  25192  ovoliunlem2  25404  mbfimaopnlem  25556  limciun  25795  ftalem3  26985  ostth3  27549  precsexlem10  28118  precsexlem11  28119  mptelee  28822  ubthlem2  30800  aciunf1lem  32586  esumcvg  34076  bnj228  34725  bnj590  34900  bnj594  34902  bnj600  34909  bnj1128  34980  bnj1125  34982  bnj1145  34983  bnj1398  35024  bnj1417  35031  dfon2lem3  35773  dfon2lem7  35777  neibastop1  36347  weiunlem2  36451  unblimceq0lem  36494  unbdqndv2  36499  rdgssun  37366  ralssiun  37395  fvineqsneu  37399  fvineqsneq  37400  cover2  37709  upixp  37723  indexdom  37728  filbcmb  37734  mettrifi  37751  mpobi123f  38156  riotasvd  38949  glbconxN  39372  cdlemefr29exN  40396  cdlemk36  40907  aks4d1p7d1  42070  mptfcl  42708  aomclem2  43044  hbtlem5  43117  gneispace  44123  trintALTVD  44869  trintALT  44870  modelaxrep  44971  refsumcn  45024  rfcnnnub  45030  choicefi  45194  mullimc  45614  mullimcf  45621  addlimc  45646  itgsubsticclem  45973  stoweidlem25  46023  stoweidlem52  46050  stoweidlem59  46057  stoweidlem62  46060  wallispilem3  46065  stirlinglem13  46084  fourierdlem73  46177  natlocalincr  46874  ffnafv  47172  iunord  49665  setrec1lem2  49677