Theorem moim

Description: The at-most-one quantifier reverses implication. (Contributed by NM, 22-Apr-1995)

	Ref	Expression
Assertion	moim	|- ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )

Proof

Step	Hyp	Ref	Expression
1		imim1	|- ( ( ph -> ps ) -> ( ( ps -> x = y ) -> ( ph -> x = y ) ) )
2	1	al2imi	|- ( A. x ( ph -> ps ) -> ( A. x ( ps -> x = y ) -> A. x ( ph -> x = y ) ) )
3	2	eximdv	|- ( A. x ( ph -> ps ) -> ( E. y A. x ( ps -> x = y ) -> E. y A. x ( ph -> x = y ) ) )
4		df-mo	|- ( E* x ps <-> E. y A. x ( ps -> x = y ) )
5		df-mo	|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
6	3 4 5	3imtr4g	|- ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )