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 ⊢ ∃! x ∃! y ∃ x φ ∧ ∃ y φ ↔ ∃! x ∃! y ∃! x φ ∧ ∃ y φ

Proof

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