Theorem eu6im

Description: One direction of eu6 needs fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023)

	Ref	Expression
Assertion	eu6im	|- ( E. y A. x ( ph <-> x = y ) -> E! x ph )

Proof

Step	Hyp	Ref	Expression
1		exsbim	|- ( E. y A. x ( x = y -> ph ) -> E. x ph )
2	1	anim1i	|- ( ( E. y A. x ( x = y -> ph ) /\ E. z A. x ( ph -> x = z ) ) -> ( E. x ph /\ E. z A. x ( ph -> x = z ) ) )
3		eu6lem	|- ( E. y A. x ( ph <-> x = y ) <-> ( E. y A. x ( x = y -> ph ) /\ E. z A. x ( ph -> x = z ) ) )
4		eu3v	|- ( E! x ph <-> ( E. x ph /\ E. z A. x ( ph -> x = z ) ) )
5	2 3 4	3imtr4i	|- ( E. y A. x ( ph <-> x = y ) -> E! x ph )