Theorem rspe 3003

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1704   ∈ wcel 1990  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-rex 2918

This theorem is referenced by:  rsp2e  3004  2rmorex  3412  ssiun2  4563  reusv2lem3  4871  tfrlem9  7481  isinf  8173  findcard2  8200  findcard3  8203  scott0  8749  ac6c4  9303  supaddc  10990  supadd  10991  supmul1  10992  supmul  10995  fsuppmapnn0fiub  12790  mreiincl  16256  restmetu  22375  bposlem3  25011  opphllem5  25643  pjpjpre  28278  atom1d  29212  actfunsnf1o  30682  bnj1398  31102  cvmlift2lem12  31296  nosupbnd1  31860  nosupbnd2  31862  finminlem  32312  neibastop2lem  32355  iooelexlt  33210  relowlpssretop  33212  prtlem18  34162  pell14qrdich  37433  eliuniin  39279  eliuniin2  39303  eliunid  39342  disjinfi  39380  iunmapsn  39409  fvelimad  39458  infnsuprnmpt  39465  upbdrech  39519  limclner  39883  limsupre3uzlem  39967  climuzlem  39975  sge0iunmptlemre  40632  iundjiun  40677  meaiininclem  40700  isomenndlem  40744  ovnsubaddlem1  40784  vonioo  40896  vonicc  40899  smfaddlem1  40971  2reurex  41181