Theorem dfeumo

Description: An elementary proof showing the reverse direction of dfmoeu . Here the characterizing expression of existential uniqueness ( eu6 ) is derived from that of uniqueness ( df-mo ). (Contributed by Wolf Lammen, 3-Oct-2023)

	Ref	Expression
Assertion	dfeumo	|- ( ( E. x ph /\ E. y A. x ( ph -> x = y ) ) <-> E. y A. x ( ph <-> x = y ) )

Proof

Step	Hyp	Ref	Expression
1		ax6ev	|- E. x x = y
2		biimpr	|- ( ( ph <-> x = y ) -> ( x = y -> ph ) )
3	2	aleximi	|- ( A. x ( ph <-> x = y ) -> ( E. x x = y -> E. x ph ) )
4	1 3	mpi	|- ( A. x ( ph <-> x = y ) -> E. x ph )
5	4	exlimiv	|- ( E. y A. x ( ph <-> x = y ) -> E. x ph )
6	5	pm4.71ri	|- ( E. y A. x ( ph <-> x = y ) <-> ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) )
7		abai	|- ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) )
8		dfmoeu	|- ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph -> x = y ) )
9	8	anbi2i	|- ( ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
10	6 7 9	3bitrri	|- ( ( E. x ph /\ E. y A. x ( ph -> x = y ) ) <-> E. y A. x ( ph <-> x = y ) )