Theorem rspe 3232

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

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

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 3061

This theorem is referenced by:  rsp2e  3260  2rmorex  3737  2reurex  3743  ssiun2  5023  reusv2lem3  5370  fvelimad  6946  tfrlem9  8399  findcard2  9178  isinf  9268  isinfOLD  9269  findcard3  9290  findcard3OLD  9291  scott0  9900  ac6c4  10495  supaddc  12209  supadd  12210  supmul1  12211  supmul  12214  fsuppmapnn0fiub  14009  mreiincl  17608  restmetu  24509  bposlem3  27249  nosupbnd1  27678  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2  27695  opphllem5  28730  pjpjpre  31400  atom1d  32334  iinabrex  32550  actfunsnf1o  34636  bnj1398  35065  cvmlift2lem12  35336  finminlem  36336  neibastop2lem  36378  iooelexlt  37380  relowlpssretop  37382  ralssiun  37425  disjlem18  38818  prtlem18  38895  pell14qrdich  42892  unielss  43242  eliuniin  45123  eliuniin2  45144  eliunid  45171  disjinfi  45216  iunmapsn  45241  infnsuprnmpt  45274  upbdrech  45334  limclner  45680  limsupre3uzlem  45764  climuzlem  45772  sge0iunmptlemre  46444  iundjiun  46489  meaiininclem  46515  isomenndlem  46559  ovnsubaddlem1  46599  vonioo  46711  vonicc  46714  smfaddlem1  46792  tworepnotupword  46915  f1oresf1o2  47320