New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  2eu5 GIF version

Theorem 2eu5 2288
 Description: An alternate definition of double existential uniqueness (see 2eu4 2287). A mistake sometimes made in the literature is to use ∃!x∃!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 ∀x∃*yφ as an additional condition. The correct definition apparently has never been published. (∃* means "exists at most one.") (Contributed by NM, 26-Oct-2003.)
Assertion
Ref Expression
2eu5 ((∃!x∃!yφ x∃*yφ) ↔ (xyφ zwxy(φ → (x = z y = w))))
Distinct variable groups:   x,y,z,w   φ,z,w
Allowed substitution hints:   φ(x,y)

Proof of Theorem 2eu5
StepHypRef Expression
1 2eu1 2284 . . 3 (x∃*yφ → (∃!x∃!yφ ↔ (∃!xyφ ∃!yxφ)))
21pm5.32ri 619 . 2 ((∃!x∃!yφ x∃*yφ) ↔ ((∃!xyφ ∃!yxφ) x∃*yφ))
3 eumo 2244 . . . . 5 (∃!yxφ∃*yxφ)
43adantl 452 . . . 4 ((∃!xyφ ∃!yxφ) → ∃*yxφ)
5 2moex 2275 . . . 4 (∃*yxφx∃*yφ)
64, 5syl 15 . . 3 ((∃!xyφ ∃!yxφ) → x∃*yφ)
76pm4.71i 613 . 2 ((∃!xyφ ∃!yxφ) ↔ ((∃!xyφ ∃!yxφ) x∃*yφ))
8 2eu4 2287 . 2 ((∃!xyφ ∃!yxφ) ↔ (xyφ zwxy(φ → (x = z y = w))))
92, 7, 83bitr2i 264 1 ((∃!x∃!yφ x∃*yφ) ↔ (xyφ zwxy(φ → (x = z y = w))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541  ∃!weu 2204  ∃*wmo 2205 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209 This theorem is referenced by:  2reu5lem3  3043
 Copyright terms: Public domain W3C validator