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

Theorem rspe 2481
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 1569 . 2  |-  ( ( x  e.  A  /\  ph )  ->  E. x
( x  e.  A  /\  ph ) )
2 df-rex 2422 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
31, 2sylibr 133 1  |-  ( ( x  e.  A  /\  ph )  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103   E.wex 1468    e. wcel 1480   E.wrex 2417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487
This theorem depends on definitions:  df-bi 116  df-rex 2422
This theorem is referenced by:  rsp2e  2483  ssiun2  3856  tfrlem9  6216  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  findcard2  6783  findcard2s  6784  prarloclemup  7315  prmuloc2  7387  ltaddpr  7417  aptiprlemu  7460  cauappcvgprlemopl  7466  cauappcvgprlemopu  7468  cauappcvgprlem2  7480  caucvgprlemopl  7489  caucvgprlemopu  7491  caucvgprlem2  7500  caucvgprprlem2  7530  suplocexprlemrl  7537  suplocexprlemru  7539  suplocexprlemlub  7544
  Copyright terms: Public domain W3C validator