Theorem rspe 2479

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 103  ∃wex 1468   ∈ wcel 1480  ∃wrex 2415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487

This theorem depends on definitions:  df-bi 116  df-rex 2420

This theorem is referenced by:  rsp2e  2481  ssiun2  3851  tfrlem9  6209  tfrlemibxssdm  6217  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  findcard2  6776  findcard2s  6777  prarloclemup  7296  prmuloc2  7368  ltaddpr  7398  aptiprlemu  7441  cauappcvgprlemopl  7447  cauappcvgprlemopu  7449  cauappcvgprlem2  7461  caucvgprlemopl  7470  caucvgprlemopu  7472  caucvgprlem2  7481  caucvgprprlem2  7511  suplocexprlemrl  7518  suplocexprlemru  7520  suplocexprlemlub  7525