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

Theorem rspe 2370
Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.)
Assertion
Ref Expression
rspe  |-  ( ( x  e.  A  /\  ph )  ->  E. x  e.  A  ph )

Proof of Theorem rspe
StepHypRef Expression
1 19.8a 1482 . 2  |-  ( ( x  e.  A  /\  ph )  ->  E. x
( x  e.  A  /\  ph ) )
2 df-rex 2312 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
31, 2sylibr 137 1  |-  ( ( x  e.  A  /\  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97   E.wex 1381    e. wcel 1393   E.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