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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 1498 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 2329 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 141 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wex 1397  wcel 1409  wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416
This theorem depends on definitions:  df-bi 114  df-rex 2329
This theorem is referenced by:  rsp2e  2389  ssiun2  3727  tfrlem9  5965  tfrlemibxssdm  5971  findcard2  6376  findcard2s  6377  prarloclemup  6650  prmuloc2  6722  ltaddpr  6752  aptiprlemu  6795  cauappcvgprlemopl  6801  cauappcvgprlemopu  6803  cauappcvgprlem2  6815  caucvgprlemopl  6824  caucvgprlemopu  6826  caucvgprlem2  6835  caucvgprprlem2  6865
  Copyright terms: Public domain W3C validator