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

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

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 1537 . 2 ((𝑥𝐴𝜑) → ∃𝑥(𝑥𝐴𝜑))
2 df-rex 2381 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
31, 2sylibr 133 1 ((𝑥𝐴𝜑) → ∃𝑥𝐴 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wex 1436  wcel 1448  wrex 2376
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455
This theorem depends on definitions:  df-bi 116  df-rex 2381
This theorem is referenced by:  rsp2e  2442  ssiun2  3803  tfrlem9  6146  tfrlemibxssdm  6154  tfr1onlembxssdm  6170  tfrcllembxssdm  6183  findcard2  6712  findcard2s  6713  prarloclemup  7204  prmuloc2  7276  ltaddpr  7306  aptiprlemu  7349  cauappcvgprlemopl  7355  cauappcvgprlemopu  7357  cauappcvgprlem2  7369  caucvgprlemopl  7378  caucvgprlemopu  7380  caucvgprlem2  7389  caucvgprprlem2  7419
  Copyright terms: Public domain W3C validator