Metamath Proof Explorer

Theorem wl-lem-nexmo

Description: This theorem provides a basic working step in proving theorems about E* or E! . (Contributed by Wolf Lammen, 3-Oct-2019)

Ref Expression
Assertion wl-lem-nexmo 
|- ( -. E. x ph -> A. x ( ph -> x = z ) )

Proof

Step Hyp Ref Expression
1 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
2 pm2.21 
 |-  ( -. ph -> ( ph -> x = z ) )
3 2 alimi 
 |-  ( A. x -. ph -> A. x ( ph -> x = z ) )
4 1 3 sylbir 
 |-  ( -. E. x ph -> A. x ( ph -> x = z ) )