Theorem rspe 2581

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1540   ∈ wcel 2202  ∃wrex 2511

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 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558

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

This theorem is referenced by:  rsp2e  2583  ssiun2  4013  tfrlem9  6485  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  findcard2  7078  findcard2s  7079  prarloclemup  7715  prmuloc2  7787  ltaddpr  7817  aptiprlemu  7860  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlem2  7880  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlem2  7900  caucvgprprlem2  7930  suplocexprlemrl  7937  suplocexprlemru  7939  suplocexprlemlub  7944