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  4036  tfrlem9  6552  tfrlemibxssdm  6560  tfr1onlembxssdm  6576  tfrcllembxssdm  6589  findcard2  7148  findcard2s  7149  prarloclemup  7815  prmuloc2  7887  ltaddpr  7917  aptiprlemu  7960  cauappcvgprlemopl  7966  cauappcvgprlemopu  7968  cauappcvgprlem2  7980  caucvgprlemopl  7989  caucvgprlemopu  7991  caucvgprlem2  8000  caucvgprprlem2  8030  suplocexprlemrl  8037  suplocexprlemru  8039  suplocexprlemlub  8044