MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspe Structured version   Visualization version   GIF version

Theorem rspe 3263
Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.)
Assertion
Ref Expression
rspe ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2178 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 3112 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 237 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wex 1781  wcel 2111  wrex 3107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175
This theorem depends on definitions:  df-bi 210  df-ex 1782  df-rex 3112
This theorem is referenced by:  rsp2e  3264  2rmorex  3693  2reurex  3698  ssiun2  4934  reusv2lem3  5266  fvelimad  6707  tfrlem9  8004  isinf  8715  findcard2  8742  findcard3  8745  scott0  9299  ac6c4  9892  supaddc  11595  supadd  11596  supmul1  11597  supmul  11600  fsuppmapnn0fiub  13354  mreiincl  16859  restmetu  23177  bposlem3  25870  opphllem5  26545  pjpjpre  29202  atom1d  30136  iinabrex  30332  actfunsnf1o  31985  bnj1398  32416  cvmlift2lem12  32674  nosupbnd1  33327  nosupbnd2  33329  finminlem  33779  neibastop2lem  33821  iooelexlt  34779  relowlpssretop  34781  ralssiun  34824  prtlem18  36173  pell14qrdich  39808  eliuniin  41733  eliuniin2  41753  eliunid  41785  disjinfi  41818  iunmapsn  41844  infnsuprnmpt  41886  upbdrech  41935  limclner  42291  limsupre3uzlem  42375  climuzlem  42383  sge0iunmptlemre  43052  iundjiun  43097  meaiininclem  43123  isomenndlem  43167  ovnsubaddlem1  43207  vonioo  43319  vonicc  43322  smfaddlem1  43394  f1oresf1o2  43845
  Copyright terms: Public domain W3C validator