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 ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w

Proof

Step Hyp Ref Expression
1 df-eu ⊢ ∃! x ∃ y φ ↔ ∃ x ∃ y φ ∧ ∃* x ∃ y φ
2 df-eu ⊢ ∃! y ∃ x φ ↔ ∃ y ∃ x φ ∧ ∃* y ∃ x φ
3 excom ⊢ ∃ y ∃ x φ ↔ ∃ x ∃ y φ
4 2 3 bianbi ⊢ ∃! y ∃ x φ ↔ ∃ x ∃ y φ ∧ ∃* y ∃ x φ
5 1 4 anbi12i ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃ x ∃ y φ ∧ ∃* x ∃ y φ ∧ ∃ x ∃ y φ ∧ ∃* y ∃ x φ
6 anandi ⊢ ∃ x ∃ y φ ∧ ∃* x ∃ y φ ∧ ∃* y ∃ x φ ↔ ∃ x ∃ y φ ∧ ∃* x ∃ y φ ∧ ∃ x ∃ y φ ∧ ∃* y ∃ x φ
7 2mo2 ⊢ ∃* x ∃ y φ ∧ ∃* y ∃ x φ ↔ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w
8 7 anbi2i ⊢ ∃ x ∃ y φ ∧ ∃* x ∃ y φ ∧ ∃* y ∃ x φ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w
9 5 6 8 3bitr2i ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w