Metamath Proof Explorer


Theorem 2eu5

Description: An alternate definition of double existential uniqueness (see 2eu4 ). A mistake sometimes made in the literature is to use E! x E! y to mean "exactly one x and exactly one y ". (For example, see Proposition 7.53 of TakeutiZaring p. 53.) It turns out that this is actually a weaker assertion, as can be seen by expanding out the formal definitions. This theorem shows that the erroneous definition can be repaired by conjoining A. x E* y ph as an additional condition. The correct definition apparently has never been published. ( E* means "there exists at most one".) (Contributed by NM, 26-Oct-2003) Avoid ax-13 . (Revised by Wolf Lammen, 2-Oct-2023)

Ref Expression
Assertion 2eu5 ∃! x ∃! y φ x * y φ x y φ z w x y φ x = z y = w

Proof

Step Hyp Ref Expression
1 2eu1v x * y φ ∃! x ∃! y φ ∃! x y φ ∃! y x φ
2 1 pm5.32ri ∃! x ∃! y φ x * y φ ∃! x y φ ∃! y x φ x * y φ
3 eumo ∃! y x φ * y x φ
4 3 adantl ∃! x y φ ∃! y x φ * y x φ
5 2moexv * y x φ x * y φ
6 4 5 syl ∃! x y φ ∃! y x φ x * y φ
7 6 pm4.71i ∃! x y φ ∃! y x φ ∃! x y φ ∃! y x φ x * y φ
8 2eu4 ∃! x y φ ∃! y x φ x y φ z w x y φ x = z y = w
9 2 7 8 3bitr2i ∃! x ∃! y φ x * y φ x y φ z w x y φ x = z y = w