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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2169 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 3068 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 233 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wex 1773  wcel 2098  wrex 3067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-ex 1774  df-rex 3068
This theorem is referenced by:  rsp2e  3273  2rmorex  3751  2reurex  3757  ssiun2  5054  reusv2lem3  5404  fvelimad  6971  tfrlem9  8412  findcard2  9195  isinf  9291  isinfOLD  9292  findcard2OLD  9315  findcard3  9316  findcard3OLD  9317  scott0  9917  ac6c4  10512  supaddc  12219  supadd  12220  supmul1  12221  supmul  12224  fsuppmapnn0fiub  13996  mreiincl  17583  restmetu  24499  bposlem3  27239  nosupbnd1  27667  nosupbnd2  27669  noinfbnd1  27682  noinfbnd2  27684  opphllem5  28575  pjpjpre  31249  atom1d  32183  iinabrex  32380  actfunsnf1o  34269  bnj1398  34698  cvmlift2lem12  34957  finminlem  35835  neibastop2lem  35877  iooelexlt  36874  relowlpssretop  36876  ralssiun  36919  disjlem18  38304  prtlem18  38381  pell14qrdich  42320  unielss  42677  eliuniin  44496  eliuniin2  44517  eliunid  44547  disjinfi  44595  iunmapsn  44620  infnsuprnmpt  44655  upbdrech  44716  limclner  45068  limsupre3uzlem  45152  climuzlem  45160  sge0iunmptlemre  45832  iundjiun  45877  meaiininclem  45903  isomenndlem  45947  ovnsubaddlem1  45987  vonioo  46099  vonicc  46102  smfaddlem1  46180  tworepnotupword  46301  f1oresf1o2  46700
  Copyright terms: Public domain W3C validator