Metamath Proof Explorer


Theorem rex0

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

Ref Expression
Assertion rex0
|- -. E. x e. (/) ph

Proof

Step Hyp Ref Expression
1 noel
 |-  -. x e. (/)
2 1 pm2.21i
 |-  ( x e. (/) -> -. ph )
3 2 nrex
 |-  -. E. x e. (/) ph