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	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-eu	⊢ ( ∃! 𝑥 ∃ 𝑦 𝜑 ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑥 ∃ 𝑦 𝜑 ) )
2		df-eu	⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 ↔ ( ∃ 𝑦 ∃ 𝑥 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) )
3		excom	⊢ ( ∃ 𝑦 ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )
4	2 3	bianbi	⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) )
5	1 4	anbi12i	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑥 ∃ 𝑦 𝜑 ) ∧ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ) )
6		anandi	⊢ ( ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ) ↔ ( ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑥 ∃ 𝑦 𝜑 ) ∧ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ) )
7		2mo2	⊢ ( ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
8	7	anbi2i	⊢ ( ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
9	5 6 8	3bitr2i	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )