Metamath Proof Explorer

Theorem nrexrmo

Description: Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017)

Ref Expression
Assertion nrexrmo 
|- ( -. E. x e. A ph -> E* x e. A ph )

Proof

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