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  6945  tfrlem9  8397  findcard2  9176  isinf  9266  isinfOLD  9267  findcard3  9288  findcard3OLD  9289  scott0  9898  ac6c4  10493  supaddc  12207  supadd  12208  supmul1  12209  supmul  12212  fsuppmapnn0fiub  14007  mreiincl  17606  restmetu  24507  bposlem3  27247  nosupbnd1  27676  nosupbnd2  27678  noinfbnd1  27691  noinfbnd2  27693  opphllem5  28676  pjpjpre  31346  atom1d  32280  iinabrex  32496  actfunsnf1o  34582  bnj1398  35011  cvmlift2lem12  35282  finminlem  36282  neibastop2lem  36324  iooelexlt  37326  relowlpssretop  37328  ralssiun  37371  disjlem18  38764  prtlem18  38841  pell14qrdich  42839  unielss  43189  eliuniin  45071  eliuniin2  45092  eliunid  45119  disjinfi  45164  iunmapsn  45189  infnsuprnmpt  45222  upbdrech  45282  limclner  45628  limsupre3uzlem  45712  climuzlem  45720  sge0iunmptlemre  46392  iundjiun  46437  meaiininclem  46463  isomenndlem  46507  ovnsubaddlem1  46547  vonioo  46659  vonicc  46662  smfaddlem1  46740  tworepnotupword  46863  f1oresf1o2  47268