Theorem rspe 3227

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

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 2008  ax-12 2178

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

This theorem is referenced by:  rsp2e  3255  2rmorex  3725  2reurex  3731  ssiun2  5011  reusv2lem3  5355  fvelimad  6928  tfrlem9  8353  findcard2  9128  isinf  9207  isinfOLD  9208  findcard3  9229  findcard3OLD  9230  scott0  9839  ac6c4  10434  supaddc  12150  supadd  12151  supmul1  12152  supmul  12155  fsuppmapnn0fiub  13956  mreiincl  17557  restmetu  24458  bposlem3  27197  nosupbnd1  27626  nosupbnd2  27628  noinfbnd1  27641  noinfbnd2  27643  opphllem5  28678  pjpjpre  31348  atom1d  32282  iinabrex  32498  actfunsnf1o  34595  bnj1398  35024  cvmlift2lem12  35301  finminlem  36306  neibastop2lem  36348  iooelexlt  37350  relowlpssretop  37352  ralssiun  37395  disjlem18  38792  prtlem18  38870  pell14qrdich  42857  unielss  43207  eliuniin  45093  eliuniin2  45114  eliunid  45141  disjinfi  45186  iunmapsn  45211  infnsuprnmpt  45244  upbdrech  45303  limclner  45649  limsupre3uzlem  45733  climuzlem  45741  sge0iunmptlemre  46413  iundjiun  46458  meaiininclem  46484  isomenndlem  46528  ovnsubaddlem1  46568  vonioo  46680  vonicc  46683  smfaddlem1  46761  tworepnotupword  46884  f1oresf1o2  47292