Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  rspe GIF version

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 1482 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 2312 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 137 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97  ∃wex 1381   ∈ wcel 1393  ∃wrex 2307 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400 This theorem depends on definitions:  df-bi 110  df-rex 2312 This theorem is referenced by:  rsp2e  2372  ssiun2  3700  tfrlem9  5935  tfrlemibxssdm  5941  findcard2  6346  findcard2s  6347  prarloclemup  6593  prmuloc2  6665  ltaddpr  6695  aptiprlemu  6738  cauappcvgprlemopl  6744  cauappcvgprlemopu  6746  cauappcvgprlem2  6758  caucvgprlemopl  6767  caucvgprlemopu  6769  caucvgprlem2  6778  caucvgprprlem2  6808
 Copyright terms: Public domain W3C validator