Metamath Proof Explorer

Theorem 2moexv

Description: Double quantification with "at most one". (Contributed by NM, 3-Dec-2001)

Ref Expression
Assertion 2moexv 
|- ( E* x E. y ph -> A. y E* x ph )

Proof

Step Hyp Ref Expression
1 nfe1 
 |-  F/ y E. y ph
2 1 nfmov 
 |-  F/ y E* x E. y ph
3 19.8a 
 |-  ( ph -> E. y ph )
4 3 moimi 
 |-  ( E* x E. y ph -> E* x ph )
5 2 4 alrimi 
 |-  ( E* x E. y ph -> A. y E* x ph )