Theorem rspe 2772

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 1793	. 2 |- ( ( x e. A /\ ph ) -> E. x ( x e. A /\ ph ) )
2		df-rex 2716	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
3	1, 2	sylibr 212	1 |- ( ( x e. A /\ ph ) -> E. x e. A ph )

Syntax hints:   -> wi 4   /\ wa 369   E.wex 1586   e. wcel 1756   E.wrex 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-rex 2716

This theorem is referenced by:  rsp2e  2774  2rmorex  3158  ssiun2  4208  reusv2lem3  4490  tfrlem9  6836  isinf  7518  findcard2  7544  findcard3  7547  scott0  8085  ac6c4  8642  supmul1  10287  supmul  10290  mreiincl  14526  restmetu  20137  bposlem3  22600  pjpjpre  24773  atom1d  25708  cvmlift2lem12  27155  supaddc  28370  supadd  28371  finminlem  28466  neibastop2lem  28534  prtlem18  28975  pell14qrdich  29163  2reurex  29958  bnj1398  31912