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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2181 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 3071 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 234 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wex 1779  wcel 2108  wrex 3070
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 2007  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3071
This theorem is referenced by:  rsp2e  3278  2rmorex  3760  2reurex  3766  ssiun2  5047  reusv2lem3  5400  fvelimad  6976  tfrlem9  8425  findcard2  9204  isinf  9296  isinfOLD  9297  findcard3  9318  findcard3OLD  9319  scott0  9926  ac6c4  10521  supaddc  12235  supadd  12236  supmul1  12237  supmul  12240  fsuppmapnn0fiub  14032  mreiincl  17639  restmetu  24583  bposlem3  27330  nosupbnd1  27759  nosupbnd2  27761  noinfbnd1  27774  noinfbnd2  27776  opphllem5  28759  pjpjpre  31438  atom1d  32372  iinabrex  32582  actfunsnf1o  34619  bnj1398  35048  cvmlift2lem12  35319  finminlem  36319  neibastop2lem  36361  iooelexlt  37363  relowlpssretop  37365  ralssiun  37408  disjlem18  38801  prtlem18  38878  pell14qrdich  42880  unielss  43230  eliuniin  45104  eliuniin2  45125  eliunid  45152  disjinfi  45197  iunmapsn  45222  infnsuprnmpt  45257  upbdrech  45317  limclner  45666  limsupre3uzlem  45750  climuzlem  45758  sge0iunmptlemre  46430  iundjiun  46475  meaiininclem  46501  isomenndlem  46545  ovnsubaddlem1  46585  vonioo  46697  vonicc  46700  smfaddlem1  46778  tworepnotupword  46901  f1oresf1o2  47303
  Copyright terms: Public domain W3C validator