This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 ↔ ∃! 𝑥 ∃ 𝑦 𝜑 ) )