Theorem 2eu1

Description: Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2eu1v when possible. (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 23-Apr-2023) (New usage is discouraged.)

	Ref	Expression
Assertion	2eu1	|- ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		2eu2ex	|- ( E! x E! y ph -> E. x E. y ph )
2		moeu	|- ( E* y ph <-> ( E. y ph -> E! y ph ) )
3	2	albii	|- ( A. x E* y ph <-> A. x ( E. y ph -> E! y ph ) )
4		euim	|- ( ( E. x E. y ph /\ A. x ( E. y ph -> E! y ph ) ) -> ( E! x E! y ph -> E! x E. y ph ) )
5	3 4	sylan2b	|- ( ( E. x E. y ph /\ A. x E* y ph ) -> ( E! x E! y ph -> E! x E. y ph ) )
6	5	ex	|- ( E. x E. y ph -> ( A. x E* y ph -> ( E! x E! y ph -> E! x E. y ph ) ) )
7	1 6	syl	|- ( E! x E! y ph -> ( A. x E* y ph -> ( E! x E! y ph -> E! x E. y ph ) ) )
8	7	pm2.43b	|- ( A. x E* y ph -> ( E! x E! y ph -> E! x E. y ph ) )
9		2euswap	|- ( A. x E* y ph -> ( E! x E. y ph -> E! y E. x ph ) )
10	8 9	syld	|- ( A. x E* y ph -> ( E! x E! y ph -> E! y E. x ph ) )
11	8 10	jcad	|- ( A. x E* y ph -> ( E! x E! y ph -> ( E! x E. y ph /\ E! y E. x ph ) ) )
12		2exeu	|- ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E! y ph )
13	11 12	impbid1	|- ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )