Metamath Proof Explorer

Theorem emptyex

Description: On the empty domain, any existentially quantified formula is false. (Contributed by Wolf Lammen, 21-Jan-2024)

Ref Expression
Assertion emptyex 
|- ( -. E. x T. -> -. E. x ph )

Proof

Step Hyp Ref Expression
1 trud 
 |-  ( ph -> T. )
2 1 eximi 
 |-  ( E. x ph -> E. x T. )
3 2 con3i 
 |-  ( -. E. x T. -> -. E. x ph )