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