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 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104  ∃wex 1545   ∈ wcel 2209  ∃wrex 2529

This proof depends on 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 proof depends on definitions:  df-bi 117  df-rex 2534

This theorem is used by:  rsp2e  2601  ssiun2  4055  tfrlem9  6594  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  findcard2  7198  findcard2s  7199  prarloclemup  7869  prmuloc2  7941  ltaddpr  7971  aptiprlemu  8014  cauappcvgprlemopl  8020  cauappcvgprlemopu  8022  cauappcvgprlem2  8034  caucvgprlemopl  8043  caucvgprlemopu  8045  caucvgprlem2  8054  caucvgprprlem2  8084  suplocexprlemrl  8091  suplocexprlemru  8093  suplocexprlemlub  8098  bposlem3  16325