Theorem euim

Description: Add unique existential quantifiers to an implication. Note the reversed implication in the antecedent. (Contributed by NM, 19-Oct-2005) (Proof shortened by Andrew Salmon, 14-Jun-2011) (Proof shortened by Wolf Lammen, 1-Oct-2023)

	Ref	Expression
Assertion	euim	|- ( ( E. x ph /\ A. x ( ph -> ps ) ) -> ( E! x ps -> E! x ph ) )

Proof

Step	Hyp	Ref	Expression
1		euimmo	|- ( A. x ( ph -> ps ) -> ( E! x ps -> E* x ph ) )
2		exmoeub	|- ( E. x ph -> ( E* x ph <-> E! x ph ) )
3	2	biimpd	|- ( E. x ph -> ( E* x ph -> E! x ph ) )
4	1 3	sylan9r	|- ( ( E. x ph /\ A. x ( ph -> ps ) ) -> ( E! x ps -> E! x ph ) )