Theorem rspe 2579

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1538   ∈ wcel 2200  ∃wrex 2509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556

This theorem depends on definitions:  df-bi 117  df-rex 2514

This theorem is referenced by:  rsp2e  2581  ssiun2  4008  tfrlem9  6476  tfrlemibxssdm  6484  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  findcard2  7064  findcard2s  7065  prarloclemup  7698  prmuloc2  7770  ltaddpr  7800  aptiprlemu  7843  cauappcvgprlemopl  7849  cauappcvgprlemopu  7851  cauappcvgprlem2  7863  caucvgprlemopl  7872  caucvgprlemopu  7874  caucvgprlem2  7883  caucvgprprlem2  7913  suplocexprlemrl  7920  suplocexprlemru  7922  suplocexprlemlub  7927