Metamath Proof Explorer

Theorem mormo

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

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

Proof

Step Hyp Ref Expression
1 moan 
 |-  ( E* x ph -> E* x ( x e. A /\ ph ) )
2 df-rmo 
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
3 1 2 sylibr 
 |-  ( E* x ph -> E* x e. A ph )