Theorem 2eu3

Description: Double existential uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 23-Apr-2023) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfmo1	|- F/ y E* y ph
2	1	19.31	|- ( A. y ( E* x ph \/ E* y ph ) <-> ( A. y E* x ph \/ E* y ph ) )
3	2	albii	|- ( A. x A. y ( E* x ph \/ E* y ph ) <-> A. x ( A. y E* x ph \/ E* y ph ) )
4		nfmo1	|- F/ x E* x ph
5	4	nfal	|- F/ x A. y E* x ph
6	5	19.32	|- ( A. x ( A. y E* x ph \/ E* y ph ) <-> ( A. y E* x ph \/ A. x E* y ph ) )
7	3 6	bitri	|- ( A. x A. y ( E* x ph \/ E* y ph ) <-> ( A. y E* x ph \/ A. x E* y ph ) )
8		2eu1	|- ( A. y E* x ph -> ( E! y E! x ph <-> ( E! y E. x ph /\ E! x E. y ph ) ) )
9	8	biimpd	|- ( A. y E* x ph -> ( E! y E! x ph -> ( E! y E. x ph /\ E! x E. y ph ) ) )
10		ancom	|- ( ( E! y E. x ph /\ E! x E. y ph ) <-> ( E! x E. y ph /\ E! y E. x ph ) )
11	9 10	imbitrdi	|- ( A. y E* x ph -> ( E! y E! x ph -> ( E! x E. y ph /\ E! y E. x ph ) ) )
12		2eu1	|- ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
13	12	biimpd	|- ( A. x E* y ph -> ( E! x E! y ph -> ( E! x E. y ph /\ E! y E. x ph ) ) )
14	11 13	jaoa	|- ( ( A. y E* x ph \/ A. x E* y ph ) -> ( ( E! y E! x ph /\ E! x E! y ph ) -> ( E! x E. y ph /\ E! y E. x ph ) ) )
15	14	ancomsd	|- ( ( A. y E* x ph \/ A. x E* y ph ) -> ( ( E! x E! y ph /\ E! y E! x ph ) -> ( E! x E. y ph /\ E! y E. x ph ) ) )
16		2exeu	|- ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E! y ph )
17		2exeu	|- ( ( E! y E. x ph /\ E! x E. y ph ) -> E! y E! x ph )
18	17	ancoms	|- ( ( E! x E. y ph /\ E! y E. x ph ) -> E! y E! x ph )
19	16 18	jca	|- ( ( E! x E. y ph /\ E! y E. x ph ) -> ( E! x E! y ph /\ E! y E! x ph ) )
20	15 19	impbid1	|- ( ( A. y E* x ph \/ A. x E* y ph ) -> ( ( E! x E! y ph /\ E! y E! x ph ) <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
21	7 20	sylbi	|- ( A. x A. y ( E* x ph \/ E* y ph ) -> ( ( E! x E! y ph /\ E! y E! x ph ) <-> ( E! x E. y ph /\ E! y E. x ph ) ) )