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

Metamath Proof Explorer

Theorem 2eu8

Description: Two equivalent expressions for double existential uniqueness. Curiously, we can put E! on either of the internal conjuncts but not both. We can also commute E! x E! y using 2eu7 . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 20-Feb-2005) (New usage is discouraged.)

Ref Expression
Assertion 2eu8 ( ∃! 𝑥 ∃! 𝑦 ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ∃! 𝑥 ∃! 𝑦 ( ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )

Proof

Step Hyp Ref Expression
1 2eu2 ⊢ ( ∃! 𝑥 ∃ 𝑦 𝜑 → ( ∃! 𝑦 ∃! 𝑥 𝜑 ↔ ∃! 𝑦 ∃ 𝑥 𝜑 ) )
2 1 pm5.32i ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) )
3 nfeu1 ⊢ Ⅎ 𝑥 ∃! 𝑥 𝜑
4 3 nfeu ⊢ Ⅎ 𝑥 ∃! 𝑦 ∃! 𝑥 𝜑
5 4 euan ⊢ ( ∃! 𝑥 ( ∃! 𝑦 ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ( ∃! 𝑦 ∃! 𝑥 𝜑 ∧ ∃! 𝑥 ∃ 𝑦 𝜑 ) )
6 ancom ⊢ ( ( ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ( ∃ 𝑦 𝜑 ∧ ∃! 𝑥 𝜑 ) )
7 6 eubii ⊢ ( ∃! 𝑦 ( ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ∃! 𝑦 ( ∃ 𝑦 𝜑 ∧ ∃! 𝑥 𝜑 ) )
8 nfe1 ⊢ Ⅎ 𝑦 ∃ 𝑦 𝜑
9 8 euan ⊢ ( ∃! 𝑦 ( ∃ 𝑦 𝜑 ∧ ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) )
10 ancom ⊢ ( ( ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) ↔ ( ∃! 𝑦 ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )
11 7 9 10 3bitri ⊢ ( ∃! 𝑦 ( ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ( ∃! 𝑦 ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )
12 11 eubii ⊢ ( ∃! 𝑥 ∃! 𝑦 ( ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ∃! 𝑥 ( ∃! 𝑦 ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )
13 ancom ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) ↔ ( ∃! 𝑦 ∃! 𝑥 𝜑 ∧ ∃! 𝑥 ∃ 𝑦 𝜑 ) )
14 5 12 13 3bitr4ri ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) ↔ ∃! 𝑥 ∃! 𝑦 ( ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )
15 2eu7 ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ∃! 𝑥 ∃! 𝑦 ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )
16 2 14 15 3bitr3ri ⊢ ( ∃! 𝑥 ∃! 𝑦 ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ∃! 𝑥 ∃! 𝑦 ( ∃! 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )