Theorem rspe 3246

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-rex 3071

This theorem is referenced by:  rsp2e  3275  2rmorex  3750  2reurex  3756  ssiun2  5050  reusv2lem3  5398  fvelimad  6959  tfrlem9  8384  findcard2  9163  isinf  9259  isinfOLD  9260  findcard2OLD  9283  findcard3  9284  findcard3OLD  9285  scott0  9880  ac6c4  10475  supaddc  12180  supadd  12181  supmul1  12182  supmul  12185  fsuppmapnn0fiub  13955  mreiincl  17539  restmetu  24078  bposlem3  26786  nosupbnd1  27214  nosupbnd2  27216  noinfbnd1  27229  noinfbnd2  27231  opphllem5  27999  pjpjpre  30667  atom1d  31601  iinabrex  31795  actfunsnf1o  33611  bnj1398  34040  cvmlift2lem12  34300  finminlem  35198  neibastop2lem  35240  iooelexlt  36238  relowlpssretop  36240  ralssiun  36283  disjlem18  37665  prtlem18  37742  pell14qrdich  41597  unielss  41957  eliuniin  43778  eliuniin2  43799  eliunid  43829  disjinfi  43881  iunmapsn  43906  infnsuprnmpt  43944  upbdrech  44005  limclner  44357  limsupre3uzlem  44441  climuzlem  44449  sge0iunmptlemre  45121  iundjiun  45166  meaiininclem  45192  isomenndlem  45236  ovnsubaddlem1  45276  vonioo  45388  vonicc  45391  smfaddlem1  45469  tworepnotupword  45590  f1oresf1o2  45989