Theorem rspe 3249

Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.)

Assertion

Ref	Expression
rspe	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Proof of Theorem rspe

Step	Hyp	Ref	Expression
1		19.8a 2181	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	1, 2	sylibr 234	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3071

This theorem is referenced by:  rsp2e  3278  2rmorex  3760  2reurex  3766  ssiun2  5047  reusv2lem3  5400  fvelimad  6976  tfrlem9  8425  findcard2  9204  isinf  9296  isinfOLD  9297  findcard3  9318  findcard3OLD  9319  scott0  9926  ac6c4  10521  supaddc  12235  supadd  12236  supmul1  12237  supmul  12240  fsuppmapnn0fiub  14032  mreiincl  17639  restmetu  24583  bposlem3  27330  nosupbnd1  27759  nosupbnd2  27761  noinfbnd1  27774  noinfbnd2  27776  opphllem5  28759  pjpjpre  31438  atom1d  32372  iinabrex  32582  actfunsnf1o  34619  bnj1398  35048  cvmlift2lem12  35319  finminlem  36319  neibastop2lem  36361  iooelexlt  37363  relowlpssretop  37365  ralssiun  37408  disjlem18  38801  prtlem18  38878  pell14qrdich  42880  unielss  43230  eliuniin  45104  eliuniin2  45125  eliunid  45152  disjinfi  45197  iunmapsn  45222  infnsuprnmpt  45257  upbdrech  45317  limclner  45666  limsupre3uzlem  45750  climuzlem  45758  sge0iunmptlemre  46430  iundjiun  46475  meaiininclem  46501  isomenndlem  46545  ovnsubaddlem1  46585  vonioo  46697  vonicc  46700  smfaddlem1  46778  tworepnotupword  46901  f1oresf1o2  47303