Theorem 2eu1v

Description: Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. Version of 2eu1 with x and y distinct, but not requiring ax-13 . (Contributed by NM, 3-Dec-2001) (Revised by Wolf Lammen, 2-Oct-2023)

	Ref	Expression
Assertion	2eu1v	|- ( 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		2euswapv	|- ( 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		2exeuv	|- ( ( 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 ) ) )