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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2109 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 3088 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 226 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wex 1742  wcel 2050  wrex 3083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106
This theorem depends on definitions:  df-bi 199  df-ex 1743  df-rex 3088
This theorem is referenced by:  rsp2e  3244  2rmorex  3648  2reurex  3653  ssiun2  4831  reusv2lem3  5148  tfrlem9  7819  isinf  8520  findcard2  8547  findcard3  8550  scott0  9103  ac6c4  9695  supaddc  11403  supadd  11404  supmul1  11405  supmul  11408  fsuppmapnn0fiub  13168  mreiincl  16719  restmetu  22877  bposlem3  25558  opphllem5  26233  pjpjpre  28971  atom1d  29905  actfunsnf1o  31523  bnj1398  31951  cvmlift2lem12  32146  nosupbnd1  32735  nosupbnd2  32737  finminlem  33187  neibastop2lem  33229  iooelexlt  34085  relowlpssretop  34087  ralssiun  34129  prtlem18  35458  pell14qrdich  38862  eliuniin  40787  eliuniin2  40809  eliunid  40841  disjinfi  40878  iunmapsn  40905  fvelimad  40945  infnsuprnmpt  40950  upbdrech  41001  limclner  41363  limsupre3uzlem  41447  climuzlem  41455  sge0iunmptlemre  42128  iundjiun  42173  meaiininclem  42199  isomenndlem  42243  ovnsubaddlem1  42283  vonioo  42395  vonicc  42398  smfaddlem1  42470  f1oresf1o2  42896
  Copyright terms: Public domain W3C validator