Metamath Proof Explorer


Theorem rexex

Description: Restricted existence implies existence. (Contributed by NM, 11-Nov-1995)

Ref Expression
Assertion rexex ( ∃ 𝑥𝐴 𝜑 → ∃ 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 df-rex ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥𝐴𝜑 ) )
2 exsimpr ( ∃ 𝑥 ( 𝑥𝐴𝜑 ) → ∃ 𝑥 𝜑 )
3 1 2 sylbi ( ∃ 𝑥𝐴 𝜑 → ∃ 𝑥 𝜑 )