Theorem 2eu2

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

	Ref	Expression
Assertion	2eu2	⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 ↔ ∃! 𝑥 ∃ 𝑦 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		eumo	⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 → ∃* 𝑦 ∃ 𝑥 𝜑 )
2		2moex	⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 → ∀ 𝑥 ∃* 𝑦 𝜑 )
3		2eu1	⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )
4		simpl	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∃! 𝑥 ∃ 𝑦 𝜑 )
5	3 4	biimtrdi	⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 → ∃! 𝑥 ∃ 𝑦 𝜑 ) )
6	1 2 5	3syl	⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 → ∃! 𝑥 ∃ 𝑦 𝜑 ) )
7		2exeu	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∃! 𝑥 ∃! 𝑦 𝜑 )
8	7	expcom	⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 → ( ∃! 𝑥 ∃ 𝑦 𝜑 → ∃! 𝑥 ∃! 𝑦 𝜑 ) )
9	6 8	impbid	⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 ↔ ∃! 𝑥 ∃ 𝑦 𝜑 ) )