Theorem rspe 2599

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1545   ∈ wcel 2209  ∃wrex 2529

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 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563

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

This theorem is referenced by:  rsp2e  2601  ssiun2  4053  tfrlem9  6584  tfrlemibxssdm  6592  tfr1onlembxssdm  6608  tfrcllembxssdm  6621  findcard2  7187  findcard2s  7188  prarloclemup  7856  prmuloc2  7928  ltaddpr  7958  aptiprlemu  8001  cauappcvgprlemopl  8007  cauappcvgprlemopu  8009  cauappcvgprlem2  8021  caucvgprlemopl  8030  caucvgprlemopu  8032  caucvgprlem2  8041  caucvgprprlem2  8071  suplocexprlemrl  8078  suplocexprlemru  8080  suplocexprlemlub  8085