Theorem rspe 2526

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1492   ∈ wcel 2148  ∃wrex 2456

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 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510

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

This theorem is referenced by:  rsp2e  2528  ssiun2  3931  tfrlem9  6322  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  findcard2  6891  findcard2s  6892  prarloclemup  7496  prmuloc2  7568  ltaddpr  7598  aptiprlemu  7641  cauappcvgprlemopl  7647  cauappcvgprlemopu  7649  cauappcvgprlem2  7661  caucvgprlemopl  7670  caucvgprlemopu  7672  caucvgprlem2  7681  caucvgprprlem2  7711  suplocexprlemrl  7718  suplocexprlemru  7720  suplocexprlemlub  7725