Theorem rspe 2440

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

Assertion

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

Proof of Theorem rspe

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

Syntax hints:   → wi 4   ∧ wa 103  ∃wex 1436   ∈ wcel 1448  ∃wrex 2376

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455

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

This theorem is referenced by:  rsp2e  2442  ssiun2  3803  tfrlem9  6146  tfrlemibxssdm  6154  tfr1onlembxssdm  6170  tfrcllembxssdm  6183  findcard2  6712  findcard2s  6713  prarloclemup  7204  prmuloc2  7276  ltaddpr  7306  aptiprlemu  7349  cauappcvgprlemopl  7355  cauappcvgprlemopu  7357  cauappcvgprlem2  7369  caucvgprlemopl  7378  caucvgprlemopu  7380  caucvgprlem2  7389  caucvgprprlem2  7419