Theorem rspe 2593

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1541   ∈ wcel 2205  ∃wrex 2523

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 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559

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

This theorem is referenced by:  rsp2e  2595  ssiun2  4039  tfrlem9  6563  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  findcard2  7159  findcard2s  7160  prarloclemup  7826  prmuloc2  7898  ltaddpr  7928  aptiprlemu  7971  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlem2  7991  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlem2  8011  caucvgprprlem2  8041  suplocexprlemrl  8048  suplocexprlemru  8050  suplocexprlemlub  8055