Type  Label  Description 
Statement 

Theorem  2exeu 1901 
Double existential uniqueness implies double uniqueness quantification.



Theorem  2mo 1902* 
Two equivalent expressions for double "at most one."



Theorem  2mos 1903* 
Double "exists at most one", using implicit substitition.



Theorem  2eu1 1904 
Double existential uniqueness. This theorem shows a condition under which
a "naive" definition matches the correct one.



Theorem  2eu2 1905 
Double existential uniqueness.



Theorem  2eu3 1906 
Double existential uniqueness.



Theorem  2eu4 1907* 
This theorem provides us with a definition of double existential
uniqueness ("exactly one and exactly one "). Naively one
might think (incorrectly) that it could be defined by
. See
2eu1 1904 for a condition under which the naive
definition holds and 2exeu 1901 for a oneway implication. See 2eu5 1908
and
2eu8 1911 for alternate definitions.



Theorem  2eu5 1908* 
An alternate definition of double existential uniqueness (see 2eu4 1907).
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.")



Theorem  2eu6 1909* 
Two equivalent expressions for double existential uniqueness.



Theorem  2eu7 1910 
Two equivalent expressions for double existential uniqueness.



Theorem  2eu8 1911 
Two equivalent expressions for double existential uniqueness. Curiously,
we can put on
either of the internal conjuncts but not both. We
can also commute using 2eu7 1910.



Theorem  euequ1 1912* 
Equality has existential uniqueness. (Contributed by Stefan Allan,
4Dec2008.)



Theorem  exists1 1913* 
Two ways to express "only one thing exists." The lefthand side
requires only one variable to express this. Both sides are false in set
theory.



Theorem  exists2 1914 
A condition implying that at least two things exist. (The proof was
shortened by Andrew Salmon, 9Jul2011.)

