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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2175 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 3071 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 233 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wex 1782  wcel 2107  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-rex 3071
This theorem is referenced by:  rsp2e  3260  2rmorex  3713  2reurex  3719  ssiun2  5008  reusv2lem3  5356  fvelimad  6910  tfrlem9  8332  findcard2  9111  isinf  9207  isinfOLD  9208  findcard2OLD  9231  findcard3  9232  findcard3OLD  9233  scott0  9827  ac6c4  10422  supaddc  12127  supadd  12128  supmul1  12129  supmul  12132  fsuppmapnn0fiub  13902  mreiincl  17481  restmetu  23942  bposlem3  26650  nosupbnd1  27078  nosupbnd2  27080  noinfbnd1  27093  noinfbnd2  27095  opphllem5  27735  pjpjpre  30403  atom1d  31337  iinabrex  31533  actfunsnf1o  33274  bnj1398  33703  cvmlift2lem12  33965  finminlem  34836  neibastop2lem  34878  iooelexlt  35879  relowlpssretop  35881  ralssiun  35924  disjlem18  37308  prtlem18  37385  pell14qrdich  41235  unielss  41595  eliuniin  43397  eliuniin2  43418  eliunid  43448  disjinfi  43500  iunmapsn  43525  infnsuprnmpt  43565  upbdrech  43626  limclner  43978  limsupre3uzlem  44062  climuzlem  44070  sge0iunmptlemre  44742  iundjiun  44787  meaiininclem  44813  isomenndlem  44857  ovnsubaddlem1  44897  vonioo  45009  vonicc  45012  smfaddlem1  45090  tworepnotupword  45211  f1oresf1o2  45609
  Copyright terms: Public domain W3C validator