Theorem rspe 2556

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1516   ∈ wcel 2177  ∃wrex 2486

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 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534

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

This theorem is referenced by:  rsp2e  2558  ssiun2  3972  tfrlem9  6412  tfrlemibxssdm  6420  tfr1onlembxssdm  6436  tfrcllembxssdm  6449  findcard2  6993  findcard2s  6994  prarloclemup  7615  prmuloc2  7687  ltaddpr  7717  aptiprlemu  7760  cauappcvgprlemopl  7766  cauappcvgprlemopu  7768  cauappcvgprlem2  7780  caucvgprlemopl  7789  caucvgprlemopu  7791  caucvgprlem2  7800  caucvgprprlem2  7830  suplocexprlemrl  7837  suplocexprlemru  7839  suplocexprlemlub  7844