Metamath Proof Explorer

Theorem nexmo1

Description: If there is no case where wff is true, it is true for at most one case. (Contributed by Peter Mazsa, 27-Sep-2021)

Ref Expression
Assertion nexmo1 
|- ( -. E. x ph -> E* x ph )

Proof

Step Hyp Ref Expression
1 pm2.21 
 |-  ( -. E. x ph -> ( E. x ph -> E! x ph ) )
2 moeu 
 |-  ( E* x ph <-> ( E. x ph -> E! x ph ) )
3 1 2 sylibr 
 |-  ( -. E. x ph -> E* x ph )