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

Theorem 2eu5 2197
 Description: An alternate definition of double existential uniqueness (see 2eu4 2196). 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 2193 . . 3
21pm5.32ri 622 . 2
3 eumo 2153 . . . . 5
43adantl 454 . . . 4
5 2moex 2184 . . . 4
64, 5syl 17 . . 3
76pm4.71i 616 . 2
8 2eu4 2196 . 2
92, 7, 83bitr2i 266 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178   wa 360  wal 1532  wex 1537  weu 2114  wmo 2115 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119
 Copyright terms: Public domain W3C validator