Theorem rspe 2844

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

Syntax hints:   -> wi 4   /\ wa 376   E.wex 1671   e. wcel 1904   E.wrex 2757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-ex 1672  df-rex 2762

This theorem is referenced by:  rsp2e  2845  2rmorex  3232  ssiun2  4312  reusv2lem3  4604  tfrlem9  7121  isinf  7803  findcard2  7829  findcard3  7832  scott0  8375  ac6c4  8929  supaddc  10596  supadd  10597  supmul1  10598  supmul  10601  mreiincl  15580  restmetu  21663  bposlem3  24293  opphllem5  24872  pjpjpre  27153  atom1d  28087  bnj1398  29915  cvmlift2lem12  30109  finminlem  31045  neibastop2lem  31087  iooelexlt  31835  relowlpssretop  31837  prtlem18  32513  pell14qrdich  35786  disjinfi  37539  iunmapsn  37570  upbdrech  37611  limclner  37829  sge0iunmptlemre  38371  iundjiun  38414  isomenndlem  38470  ovnsubaddlem1  38510  2reurex  38747