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

Theorem rspe 2387
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 1498 . 2  |-  ( ( x  e.  A  /\  ph )  ->  E. x
( x  e.  A  /\  ph ) )
2 df-rex 2329 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
31, 2sylibr 141 1  |-  ( ( x  e.  A  /\  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101   E.wex 1397    e. wcel 1409   E.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  3728  tfrlem9  5966  tfrlemibxssdm  5972  findcard2  6377  findcard2s  6378  prarloclemup  6651  prmuloc2  6723  ltaddpr  6753  aptiprlemu  6796  cauappcvgprlemopl  6802  cauappcvgprlemopu  6804  cauappcvgprlem2  6816  caucvgprlemopl  6825  caucvgprlemopu  6827  caucvgprlem2  6836  caucvgprprlem2  6866
  Copyright terms: Public domain W3C validator