Theorem 2eu4

Description: This theorem provides us with a definition of double existential uniqueness ("exactly one x and exactly one y "). Naively one might think (incorrectly) that it could be defined by E! x E! y ph . See 2eu1 for a condition under which the naive definition holds and 2exeu for a one-way implication. See 2eu5 and 2eu8 for alternate definitions. (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 14-Sep-2019)

	Ref	Expression
Assertion	2eu4	|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-eu	|- ( E! x E. y ph <-> ( E. x E. y ph /\ E* x E. y ph ) )
2		df-eu	|- ( E! y E. x ph <-> ( E. y E. x ph /\ E* y E. x ph ) )
3		excom	|- ( E. y E. x ph <-> E. x E. y ph )
4	3	anbi1i	|- ( ( E. y E. x ph /\ E* y E. x ph ) <-> ( E. x E. y ph /\ E* y E. x ph ) )
5	2 4	bitri	|- ( E! y E. x ph <-> ( E. x E. y ph /\ E* y E. x ph ) )
6	1 5	anbi12i	|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( ( E. x E. y ph /\ E* x E. y ph ) /\ ( E. x E. y ph /\ E* y E. x ph ) ) )
7		anandi	|- ( ( E. x E. y ph /\ ( E* x E. y ph /\ E* y E. x ph ) ) <-> ( ( E. x E. y ph /\ E* x E. y ph ) /\ ( E. x E. y ph /\ E* y E. x ph ) ) )
8		2mo2	|- ( ( E* x E. y ph /\ E* y E. x ph ) <-> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
9	8	anbi2i	|- ( ( E. x E. y ph /\ ( E* x E. y ph /\ E* y E. x ph ) ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
10	6 7 9	3bitr2i	|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )