Metamath Proof Explorer

Theorem 2eumo

Description: Nested unique existential quantifier and at-most-one quantifier. (Contributed by NM, 3-Dec-2001)

Ref Expression
Assertion 2eumo 
|- ( E! x E* y ph -> E* x E! y ph )

Proof

Step Hyp Ref Expression
1 euimmo 
 |-  ( A. x ( E! y ph -> E* y ph ) -> ( E! x E* y ph -> E* x E! y ph ) )
2 eumo 
 |-  ( E! y ph -> E* y ph )
3 1 2 mpg 
 |-  ( E! x E* y ph -> E* x E! y ph )