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

Metamath Proof Explorer

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