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