Theorem dfmoeu

Description: An elementary proof of moeu in disguise, connecting an expression characterizing uniqueness ( df-mo ) to that of existential uniqueness ( eu6 ). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo . (Contributed by Wolf Lammen, 27-May-2019)

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

Proof

Step	Hyp	Ref	Expression
1		alnex	|- ( A. x -. ph <-> -. E. x ph )
2		pm2.21	|- ( -. ph -> ( ph -> x = y ) )
3	2	alimi	|- ( A. x -. ph -> A. x ( ph -> x = y ) )
4	1 3	sylbir	|- ( -. E. x ph -> A. x ( ph -> x = y ) )
5	4	19.8ad	|- ( -. E. x ph -> E. y A. x ( ph -> x = y ) )
6		biimp	|- ( ( ph <-> x = y ) -> ( ph -> x = y ) )
7	6	alimi	|- ( A. x ( ph <-> x = y ) -> A. x ( ph -> x = y ) )
8	7	eximi	|- ( E. y A. x ( ph <-> x = y ) -> E. y A. x ( ph -> x = y ) )
9	5 8	ja	|- ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) -> E. y A. x ( ph -> x = y ) )
10		nfia1	|- F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) )
11		id	|- ( ph -> ph )
12		ax12v	|- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
13	12	com12	|- ( ph -> ( x = y -> A. x ( x = y -> ph ) ) )
14	11 13	embantd	|- ( ph -> ( ( ph -> x = y ) -> A. x ( x = y -> ph ) ) )
15	14	spsd	|- ( ph -> ( A. x ( ph -> x = y ) -> A. x ( x = y -> ph ) ) )
16	15	ancld	|- ( ph -> ( A. x ( ph -> x = y ) -> ( A. x ( ph -> x = y ) /\ A. x ( x = y -> ph ) ) ) )
17		albiim	|- ( A. x ( ph <-> x = y ) <-> ( A. x ( ph -> x = y ) /\ A. x ( x = y -> ph ) ) )
18	16 17	syl6ibr	|- ( ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) )
19	10 18	exlimi	|- ( E. x ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) )
20	19	eximdv	|- ( E. x ph -> ( E. y A. x ( ph -> x = y ) -> E. y A. x ( ph <-> x = y ) ) )
21	20	com12	|- ( E. y A. x ( ph -> x = y ) -> ( E. x ph -> E. y A. x ( ph <-> x = y ) ) )
22	9 21	impbii	|- ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph -> x = y ) )