Theorem rspe 3261

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1806   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-rex 3096

This theorem is referenced by:  rsp2e  3289  2rmorex  3726  2reurex  3732  ssiun2  5016  reusv2lem3  5372  fvelimad  6949  tfrlem9  8372  findcard2  9149  isinf  9225  findcard3  9243  scott0  9860  ac6c4  10465  supaddc  12182  supadd  12183  supmul1  12184  supmul  12187  fsuppmapnn0fiub  14027  mreiincl  17648  restmetu  24696  bposlem3  27416  nosupbnd1  27844  nosupbnd2  27846  noinfbnd1  27859  noinfbnd2  27861  opphllem5  28991  pjpjpre  31712  atom1d  32646  iinabrex  32855  actfunsnf1o  34936  bnj1398  35367  cvmlift2lem12  35705  finminlem  36718  neibastop2lem  36760  iooelexlt  37896  relowlpssretop  37898  ralssiun  37941  disjlem18  39442  prtlem18  39541  pell14qrdich  43488  unielss  43837  eliuniin  45709  eliuniin2  45730  eliunid  45757  disjinfi  45802  iunmapsn  45825  infnsuprnmpt  45857  upbdrech  45916  limclner  46257  limsupre3uzlem  46341  climuzlem  46349  sge0iunmptlemre  47021  iundjiun  47066  meaiininclem  47092  isomenndlem  47136  ovnsubaddlem1  47176  vonioo  47288  vonicc  47291  smfaddlem1  47369  f1oresf1o2  47917