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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2215 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 3088 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 237 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 400  wex 1807  wcel 2141  wrex 3087
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-12 2211
This theorem depends on definitions:  df-bi 210  df-ex 1808  df-rex 3088
This theorem is referenced by:  rsp2e  3281  2rmorex  3716  2reurex  3722  ssiun2  5011  reusv2lem3  5371  fvelimad  6948  tfrlem9  8371  findcard2  9148  isinf  9224  findcard3  9242  scott0  9859  ac6c4  10464  supaddc  12181  supadd  12182  supmul1  12183  supmul  12186  fsuppmapnn0fiub  14027  mreiincl  17647  restmetu  24706  bposlem3  27426  nosupbnd1  27854  nosupbnd2  27856  noinfbnd1  27869  noinfbnd2  27871  opphllem5  29007  dfprlng2  29170  pjpjpre  31737  atom1d  32671  iinabrex  32880  actfunsnf1o  34957  bnj1398  35388  cvmlift2lem12  35772  finminlem  36795  neibastop2lem  36837  iooelexlt  37974  relowlpssretop  37976  ralssiun  38019  disjlem18  39520  prtlem18  39619  pell14qrdich  43566  unielss  43915  eliuniin  45787  eliuniin2  45808  eliunid  45835  disjinfi  45880  iunmapsn  45903  infnsuprnmpt  45935  upbdrech  45994  limclner  46335  limsupre3uzlem  46419  climuzlem  46427  sge0iunmptlemre  47099  iundjiun  47144  meaiininclem  47170  isomenndlem  47214  ovnsubaddlem1  47254  vonioo  47366  vonicc  47369  smfaddlem1  47447  f1oresf1o2  47995
  Copyright terms: Public domain W3C validator