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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2090 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 2947 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 224 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wex 1744  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-rex 2947
This theorem is referenced by:  rsp2e  3033  2rmorex  3445  ssiun2  4595  reusv2lem3  4901  tfrlem9  7526  isinf  8214  findcard2  8241  findcard3  8244  scott0  8787  ac6c4  9341  supaddc  11028  supadd  11029  supmul1  11030  supmul  11033  fsuppmapnn0fiub  12830  mreiincl  16303  restmetu  22422  bposlem3  25056  opphllem5  25688  pjpjpre  28406  atom1d  29340  actfunsnf1o  30810  bnj1398  31228  cvmlift2lem12  31422  nosupbnd1  31985  nosupbnd2  31987  finminlem  32437  neibastop2lem  32480  iooelexlt  33340  relowlpssretop  33342  prtlem18  34481  pell14qrdich  37750  eliuniin  39593  eliuniin2  39617  eliunid  39656  disjinfi  39694  iunmapsn  39723  fvelimad  39772  infnsuprnmpt  39779  upbdrech  39833  limclner  40201  limsupre3uzlem  40285  climuzlem  40293  sge0iunmptlemre  40950  iundjiun  40995  meaiininclem  41021  isomenndlem  41065  ovnsubaddlem1  41105  vonioo  41217  vonicc  41220  smfaddlem1  41292  2reurex  41502
  Copyright terms: Public domain W3C validator