Theorem rspe 2580

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 2515	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	1, 2	sylibr 134	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1540   ∈ wcel 2201  ∃wrex 2510

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 2515

This theorem is referenced by:  rsp2e  2582  ssiun2  4014  tfrlem9  6490  tfrlemibxssdm  6498  tfr1onlembxssdm  6514  tfrcllembxssdm  6527  findcard2  7083  findcard2s  7084  prarloclemup  7720  prmuloc2  7792  ltaddpr  7822  aptiprlemu  7865  cauappcvgprlemopl  7871  cauappcvgprlemopu  7873  cauappcvgprlem2  7885  caucvgprlemopl  7894  caucvgprlemopu  7896  caucvgprlem2  7905  caucvgprprlem2  7935  suplocexprlemrl  7942  suplocexprlemru  7944  suplocexprlemlub  7949