Theorem rspe 2412

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

Step	Hyp	Ref	Expression
1		19.8a 1522	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2354	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
3	1, 2	sylibr 132	1 |- ( ( x e. A /\ ph ) -> E. x e. A ph )

Syntax hints:   -> wi 4   /\ wa 102   E.wex 1421   e. wcel 1433   E.wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440

This theorem depends on definitions:  df-bi 115  df-rex 2354

This theorem is referenced by:  rsp2e  2414  ssiun2  3721  tfrlem9  5958  tfrlemibxssdm  5964  findcard2  6373  findcard2s  6374  prarloclemup  6685  prmuloc2  6757  ltaddpr  6787  aptiprlemu  6830  cauappcvgprlemopl  6836  cauappcvgprlemopu  6838  cauappcvgprlem2  6850  caucvgprlemopl  6859  caucvgprlemopu  6861  caucvgprlem2  6870  caucvgprprlem2  6900