This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rex0

Description: Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003)

Ref Expression
Assertion rex0 ¬ ∃ 𝑥 ∈ ∅ 𝜑

Proof

Step Hyp Ref Expression
1 noel ⊢ ¬ 𝑥 ∈ ∅
2 1 pm2.21i ⊢ ( 𝑥 ∈ ∅ → ¬ 𝜑 )
3 2 nrex ⊢ ¬ ∃ 𝑥 ∈ ∅ 𝜑