Theorem rspe 3237

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 3070	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	1, 2	sylibr 233	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1782   ∈ wcel 2106  ∃wrex 3065

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

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-rex 3070

This theorem is referenced by:  rsp2e  3238  2rmorex  3689  2reurex  3695  ssiun2  4977  reusv2lem3  5323  fvelimad  6836  tfrlem9  8216  findcard2  8947  isinf  9036  findcard2OLD  9056  findcard3  9057  scott0  9644  ac6c4  10237  supaddc  11942  supadd  11943  supmul1  11944  supmul  11947  fsuppmapnn0fiub  13711  mreiincl  17305  restmetu  23726  bposlem3  26434  opphllem5  27112  pjpjpre  29781  atom1d  30715  iinabrex  30908  actfunsnf1o  32584  bnj1398  33014  cvmlift2lem12  33276  nosupbnd1  33917  nosupbnd2  33919  noinfbnd1  33932  noinfbnd2  33934  finminlem  34507  neibastop2lem  34549  iooelexlt  35533  relowlpssretop  35535  ralssiun  35578  prtlem18  36891  pell14qrdich  40691  eliuniin  42649  eliuniin2  42669  eliunid  42699  disjinfi  42731  iunmapsn  42757  infnsuprnmpt  42796  upbdrech  42844  limclner  43192  limsupre3uzlem  43276  climuzlem  43284  sge0iunmptlemre  43953  iundjiun  43998  meaiininclem  44024  isomenndlem  44068  ovnsubaddlem1  44108  vonioo  44220  vonicc  44223  smfaddlem1  44298  f1oresf1o2  44783  tworepnotupword  46521