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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2206 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 3067 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 224 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wex 1852  wcel 2145  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-ex 1853  df-rex 3067
This theorem is referenced by:  rsp2e  3152  2rmorex  3564  ssiun2  4697  reusv2lem3  5000  tfrlem9  7634  isinf  8329  findcard2  8356  findcard3  8359  scott0  8913  ac6c4  9505  supaddc  11192  supadd  11193  supmul1  11194  supmul  11197  fsuppmapnn0fiub  12998  mreiincl  16464  restmetu  22595  bposlem3  25232  opphllem5  25864  pjpjpre  28618  atom1d  29552  actfunsnf1o  31022  bnj1398  31440  cvmlift2lem12  31634  nosupbnd1  32197  nosupbnd2  32199  finminlem  32649  neibastop2lem  32692  iooelexlt  33547  relowlpssretop  33549  prtlem18  34685  pell14qrdich  37959  eliuniin  39800  eliuniin2  39824  eliunid  39862  disjinfi  39900  iunmapsn  39927  fvelimad  39976  infnsuprnmpt  39983  upbdrech  40036  limclner  40401  limsupre3uzlem  40485  climuzlem  40493  sge0iunmptlemre  41149  iundjiun  41194  meaiininclem  41220  isomenndlem  41264  ovnsubaddlem1  41304  vonioo  41416  vonicc  41419  smfaddlem1  41491  2reurex  41701  f1oresf1o2  41833
  Copyright terms: Public domain W3C validator