Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2eu5 Unicode version

Theorem 2eu5 2338
 Description: An alternate definition of double existential uniqueness (see 2eu4 2337). A mistake sometimes made in the literature is to use to mean "exactly one and exactly one ." (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 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
Distinct variable groups:   ,,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem 2eu5
StepHypRef Expression
1 2eu1 2334 . . 3
21pm5.32ri 620 . 2
3 eumo 2294 . . . . 5
43adantl 453 . . . 4
5 2moex 2325 . . . 4
64, 5syl 16 . . 3
76pm4.71i 614 . 2
8 2eu4 2337 . 2
92, 7, 83bitr2i 265 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wal 1546  wex 1547  weu 2254  wmo 2255 This theorem is referenced by:  2reu5lem3  3101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259
 Copyright terms: Public domain W3C validator