Theorem rspe 3228

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3054

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 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3055

This theorem is referenced by:  rsp2e  3256  2rmorex  3728  2reurex  3734  ssiun2  5014  reusv2lem3  5358  fvelimad  6931  tfrlem9  8356  findcard2  9134  isinf  9214  isinfOLD  9215  findcard3  9236  findcard3OLD  9237  scott0  9846  ac6c4  10441  supaddc  12157  supadd  12158  supmul1  12159  supmul  12162  fsuppmapnn0fiub  13963  mreiincl  17564  restmetu  24465  bposlem3  27204  nosupbnd1  27633  nosupbnd2  27635  noinfbnd1  27648  noinfbnd2  27650  opphllem5  28685  pjpjpre  31355  atom1d  32289  iinabrex  32505  actfunsnf1o  34602  bnj1398  35031  cvmlift2lem12  35308  finminlem  36313  neibastop2lem  36355  iooelexlt  37357  relowlpssretop  37359  ralssiun  37402  disjlem18  38799  prtlem18  38877  pell14qrdich  42864  unielss  43214  eliuniin  45100  eliuniin2  45121  eliunid  45148  disjinfi  45193  iunmapsn  45218  infnsuprnmpt  45251  upbdrech  45310  limclner  45656  limsupre3uzlem  45740  climuzlem  45748  sge0iunmptlemre  46420  iundjiun  46465  meaiininclem  46491  isomenndlem  46535  ovnsubaddlem1  46575  vonioo  46687  vonicc  46690  smfaddlem1  46768  tworepnotupword  46891  f1oresf1o2  47296