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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 2039 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 2902 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 223 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-rex 2902 This theorem is referenced by:  rsp2e  2987  2rmorex  3379  ssiun2  4499  reusv2lem3  4797  tfrlem9  7368  isinf  8058  findcard2  8085  findcard3  8088  scott0  8632  ac6c4  9186  supaddc  10867  supadd  10868  supmul1  10869  supmul  10872  fsuppmapnn0fiub  12652  mreiincl  16079  restmetu  22185  bposlem3  24811  opphllem5  25443  pjpjpre  27662  atom1d  28596  bnj1398  30356  cvmlift2lem12  30550  finminlem  31482  neibastop2lem  31525  iooelexlt  32386  relowlpssretop  32388  prtlem18  33180  pell14qrdich  36451  eliuniin  38307  eliuniin2  38335  disjinfi  38375  iunmapsn  38404  upbdrech  38460  limclner  38718  sge0iunmptlemre  39308  iundjiun  39353  meaiininclem  39376  isomenndlem  39420  ovnsubaddlem1  39460  vonioo  39573  vonicc  39576  smfaddlem1  39649  2reurex  39830
 Copyright terms: Public domain W3C validator