Theorem List for Intuitionistic Logic Explorer - 2001-2100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nf5-1 2001 |
One direction of nf5 . (Contributed by Wolf Lammen, 16-Sep-2021.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | nf5d 2002 |
Deduce that is not
free in in a
context. (Contributed by
Mario Carneiro, 24-Sep-2016.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
1.4.6 Existential uniqueness
|
|
Syntax | weu 2003 |
Extend wff definition to include existential uniqueness ("there exists a
unique such that
").
|
![E! E!](_e1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) |
|
Syntax | wmo 2004 |
Extend wff definition to include uniqueness ("there exists at most one
such that ").
|
![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) |
|
Theorem | eujust 2005* |
A soundness justification theorem for df-eu 2006, showing that the
definition is equivalent to itself with its dummy variable renamed.
Note that and
needn't be distinct
variables. (Contributed
by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif)
![y y](_y.gif) ![E.
E.](exists.gif) ![z z](_z.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif)
![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Definition | df-eu 2006* |
Define existential uniqueness, i.e. "there exists exactly one
such that ." Definition 10.1 of [BellMachover] p. 97; also
Definition *14.02 of [WhiteheadRussell] p. 175. Other possible
definitions are given by eu1 2028, eu2 2047, eu3 2049,
and eu5 2050 (which in
some cases we show with a hypothesis ![A. A.](forall.gif) ![y y](_y.gif) in place of a
distinct variable condition on and ). Double uniqueness is
tricky: ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) does
not mean "exactly one and one
" (see 2eu4 2096). (Contributed by NM, 5-Aug-1993.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Definition | df-mo 2007 |
Define "there exists at most one such that ." Here we define
it in terms of existential uniqueness. Notation of [BellMachover] p. 460,
whose definition we show as mo3 2057. For another possible definition see
mo4 2064. (Contributed by NM, 5-Aug-1993.)
|
![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | euf 2008* |
A version of the existential uniqueness definition with a hypothesis
instead of a distinct variable condition. (Contributed by NM,
12-Aug-1993.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eubidh 2009 |
Formula-building rule for unique existential quantifier (deduction
form). (Contributed by NM, 9-Jul-1994.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | eubid 2010 |
Formula-building rule for unique existential quantifier (deduction
form). (Contributed by NM, 9-Jul-1994.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | eubidv 2011* |
Formula-building rule for unique existential quantifier (deduction
form). (Contributed by NM, 9-Jul-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | eubii 2012 |
Introduce unique existential quantifier to both sides of an equivalence.
(Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro,
6-Oct-2016.)
|
![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | hbeu1 2013 |
Bound-variable hypothesis builder for uniqueness. (Contributed by NM,
9-Jul-1994.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | nfeu1 2014 |
Bound-variable hypothesis builder for uniqueness. (Contributed by NM,
9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) |
|
Theorem | nfmo1 2015 |
Bound-variable hypothesis builder for "at most one." (Contributed by
NM,
8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) |
|
Theorem | sb8eu 2016 |
Variable substitution in unique existential quantifier. (Contributed by
NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | sb8mo 2017 |
Variable substitution for "at most one." (Contributed by Alexander
van
der Vekens, 17-Jun-2017.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | nfeudv 2018* |
Deduction version of nfeu 2022. Similar to nfeud 2019 but has the additional
constraint that
and must be distinct.
(Contributed by Jim
Kingdon, 25-May-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | nfeud 2019 |
Deduction version of nfeu 2022. (Contributed by NM, 15-Feb-2013.)
(Revised by Mario Carneiro, 7-Oct-2016.) (Proof rewritten by Jim
Kingdon, 25-May-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | nfmod 2020 |
Bound-variable hypothesis builder for "at most one." (Contributed by
Mario Carneiro, 14-Nov-2016.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | nfeuv 2021* |
Bound-variable hypothesis builder for existential uniqueness. This is
similar to nfeu 2022 but has the additional constraint that and
must be distinct. (Contributed by Jim Kingdon, 23-May-2018.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![F/
F/](finv.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) |
|
Theorem | nfeu 2022 |
Bound-variable hypothesis builder for existential uniqueness. Note that
and needn't be distinct.
(Contributed by NM, 8-Mar-1995.)
(Revised by Mario Carneiro, 7-Oct-2016.) (Proof rewritten by Jim
Kingdon, 23-May-2018.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![F/
F/](finv.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) |
|
Theorem | nfmo 2023 |
Bound-variable hypothesis builder for "at most one." (Contributed by
NM, 9-Mar-1995.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![F/
F/](finv.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) |
|
Theorem | hbeu 2024 |
Bound-variable hypothesis builder for uniqueness. Note that and
needn't be
distinct. (Contributed by NM, 8-Mar-1995.) (Proof
rewritten by Jim Kingdon, 24-May-2018.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | hbeud 2025 |
Deduction version of hbeu 2024. (Contributed by NM, 15-Feb-2013.) (Proof
rewritten by Jim Kingdon, 25-May-2018.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![E! E!](_e1.gif) ![y y](_y.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sb8euh 2026 |
Variable substitution in unique existential quantifier. (Contributed by
NM, 7-Aug-1994.) (Revised by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | cbveu 2027 |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | eu1 2028* |
An alternate way to express uniqueness used by some authors. Exercise
2(b) of [Margaris] p. 110.
(Contributed by NM, 20-Aug-1993.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | euor 2029 |
Introduce a disjunct into a unique existential quantifier. (Contributed
by NM, 21-Oct-2005.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![E!
E!](_e1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | euorv 2030* |
Introduce a disjunct into a unique existential quantifier. (Contributed
by NM, 23-Mar-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![E!
E!](_e1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mo2n 2031* |
There is at most one of something which does not exist. (Contributed by
Jim Kingdon, 2-Jul-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif)
![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mon 2032 |
There is at most one of something which does not exist. (Contributed by
Jim Kingdon, 5-Jul-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | euex 2033 |
Existential uniqueness implies existence. (Contributed by NM,
15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | eumo0 2034* |
Existential uniqueness implies "at most one." (Contributed by NM,
8-Jul-1994.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif)
![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eumo 2035 |
Existential uniqueness implies "at most one." (Contributed by NM,
23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | eumoi 2036 |
"At most one" inferred from existential uniqueness. (Contributed by
NM,
5-Apr-1995.)
|
![E!
E!](_e1.gif) ![x x](_x.gif) ![E*
E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) |
|
Theorem | mobidh 2037 |
Formula-building rule for "at most one" quantifier (deduction form).
(Contributed by NM, 8-Mar-1995.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | mobid 2038 |
Formula-building rule for "at most one" quantifier (deduction form).
(Contributed by NM, 8-Mar-1995.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | mobidv 2039* |
Formula-building rule for "at most one" quantifier (deduction form).
(Contributed by Mario Carneiro, 7-Oct-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | mobii 2040 |
Formula-building rule for "at most one" quantifier (inference form).
(Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro,
17-Oct-2016.)
|
![( (](lp.gif) ![ch ch](_chi.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ch ch](_chi.gif) ![) )](rp.gif) |
|
Theorem | hbmo1 2041 |
Bound-variable hypothesis builder for "at most one." (Contributed by
NM,
8-Mar-1995.)
|
![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | hbmo 2042 |
Bound-variable hypothesis builder for "at most one." (Contributed by
NM, 9-Mar-1995.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | cbvmo 2043 |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon,
8-Jun-2011.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | mo23 2044* |
An implication between two definitions of "there exists at most one."
(Contributed by Jim Kingdon, 25-Jun-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif)
![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif)
![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mor 2045* |
Converse of mo23 2044 with an additional ![E. E.](exists.gif) ![x x](_x.gif) condition.
(Contributed by Jim Kingdon, 25-Jun-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![[
[](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modc 2046* |
Equivalent definitions of "there exists at most one," given decidable
existence. (Contributed by Jim Kingdon, 1-Jul-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) DECID ![E.
E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif)
![y y](_y.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![(
(](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif)
![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif)
![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eu2 2047* |
An alternate way of defining existential uniqueness. Definition 6.10 of
[TakeutiZaring] p. 26.
(Contributed by NM, 8-Jul-1994.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eu3h 2048* |
An alternate way to express existential uniqueness. (Contributed by NM,
8-Jul-1994.) (New usage is discouraged.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eu3 2049* |
An alternate way to express existential uniqueness. (Contributed by NM,
8-Jul-1994.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eu5 2050 |
Uniqueness in terms of "at most one." (Contributed by NM,
23-Mar-1995.)
(Proof rewritten by Jim Kingdon, 27-May-2018.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | exmoeu2 2051 |
Existence implies "at most one" is equivalent to uniqueness.
(Contributed
by NM, 5-Apr-2004.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | moabs 2052 |
Absorption of existence condition by "at most one." (Contributed by
NM,
4-Nov-2002.)
|
![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | exmodc 2053 |
If existence is decidable, something exists or at most one exists.
(Contributed by Jim Kingdon, 30-Jun-2018.)
|
DECID ![E.
E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | exmonim 2054 |
There is at most one of something which does not exist. Unlike exmodc 2053
there is no decidability condition. (Contributed by Jim Kingdon,
22-Sep-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | mo2r 2055* |
A condition which implies "at most one." (Contributed by Jim
Kingdon,
2-Jul-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![y y](_y.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | mo3h 2056* |
Alternate definition of "at most one." Definition of [BellMachover]
p. 460, except that definition has the side condition that not
occur in
in place of our hypothesis. (Contributed by NM,
8-Mar-1995.) (New usage is discouraged.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mo3 2057* |
Alternate definition of "at most one." Definition of [BellMachover]
p. 460, except that definition has the side condition that not
occur in
in place of our hypothesis. (Contributed by NM,
8-Mar-1995.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mo2dc 2058* |
Alternate definition of "at most one" where existence is decidable.
(Contributed by Jim Kingdon, 2-Jul-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) DECID ![E.
E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif)
![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | euan 2059 |
Introduction of a conjunct into unique existential quantifier.
(Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon,
9-Jul-2011.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![( (](lp.gif)
![E! E!](_e1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | euanv 2060* |
Introduction of a conjunct into unique existential quantifier.
(Contributed by NM, 23-Mar-1995.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![( (](lp.gif)
![E! E!](_e1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | euor2 2061 |
Introduce or eliminate a disjunct in a unique existential quantifier.
(Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon,
9-Jul-2011.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sbmo 2062* |
Substitution into "at most one". (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![E* E*](_em1.gif) ![z z](_z.gif) ![E* E*](_em1.gif) ![z z](_z.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | mo4f 2063* |
"At most one" expressed using implicit substitution. (Contributed by
NM, 10-Apr-2004.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mo4 2064* |
"At most one" expressed using implicit substitution. (Contributed by
NM, 26-Jul-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eu4 2065* |
Uniqueness using implicit substitution. (Contributed by NM,
26-Jul-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | exmoeudc 2066 |
Existence in terms of "at most one" and uniqueness. (Contributed by
Jim
Kingdon, 3-Jul-2018.)
|
DECID ![E.
E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | moim 2067 |
"At most one" is preserved through implication (notice wff reversal).
(Contributed by NM, 22-Apr-1995.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | moimi 2068 |
"At most one" is preserved through implication (notice wff reversal).
(Contributed by NM, 15-Feb-2006.)
|
![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | moimv 2069* |
Move antecedent outside of "at most one." (Contributed by NM,
28-Jul-1995.)
|
![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | euimmo 2070 |
Uniqueness implies "at most one" through implication. (Contributed
by NM,
22-Apr-1995.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | euim 2071 |
Add existential unique existential quantifiers to an implication. Note
the reversed implication in the antecedent. (Contributed by NM,
19-Oct-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | moan 2072 |
"At most one" is still the case when a conjunct is added.
(Contributed by
NM, 22-Apr-1995.)
|
![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | moani 2073 |
"At most one" is still true when a conjunct is added. (Contributed
by
NM, 9-Mar-1995.)
|
![E*
E*](_em1.gif) ![x x](_x.gif) ![E*
E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | moor 2074 |
"At most one" is still the case when a disjunct is removed.
(Contributed
by NM, 5-Apr-2004.)
|
![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | mooran1 2075 |
"At most one" imports disjunction to conjunction. (Contributed by
NM,
5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps
ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mooran2 2076 |
"At most one" exports disjunction to conjunction. (Contributed by
NM,
5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E*
E*](_em1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | moanim 2077 |
Introduction of a conjunct into at-most-one quantifier. (Contributed by
NM, 3-Dec-2001.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | moanimv 2078* |
Introduction of a conjunct into at-most-one quantifier. (Contributed by
NM, 23-Mar-1995.)
|
![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | moaneu 2079 |
Nested at-most-one and unique existential quantifiers. (Contributed by
NM, 25-Jan-2006.)
|
![E*
E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E!
E!](_e1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | moanmo 2080 |
Nested at-most-one quantifiers. (Contributed by NM, 25-Jan-2006.)
|
![E*
E*](_em1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E*
E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | mopick 2081 |
"At most one" picks a variable value, eliminating an existential
quantifier. (Contributed by NM, 27-Jan-1997.)
|
![( (](lp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps
ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | eupick 2082 |
Existential uniqueness "picks" a variable value for which another wff
is
true. If there is only one thing such that is true, and
there is also an
(actually the same one) such that and
are both true, then implies regardless of . This
theorem can be useful for eliminating existential quantifiers in a
hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192.
(Contributed by NM, 10-Jul-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps
ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | eupicka 2083 |
Version of eupick 2082 with closed formulas. (Contributed by NM,
6-Sep-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps
ps](_psi.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eupickb 2084 |
Existential uniqueness "pick" showing wff equivalence. (Contributed
by
NM, 25-Nov-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eupickbi 2085 |
Theorem *14.26 in [WhiteheadRussell]
p. 192. (Contributed by Andrew
Salmon, 11-Jul-2011.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif)
![ps ps](_psi.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mopick2 2086 |
"At most one" can show the existence of a common value. In this case
we
can infer existence of conjunction from a conjunction of existence, and it
is one way to achieve the converse of 19.40 1608. (Contributed by NM,
5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps
ps](_psi.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif)
![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | moexexdc 2087 |
"At most one" double quantification. (Contributed by Jim Kingdon,
5-Jul-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) DECID ![E.
E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![A.
A.](forall.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![ps ps](_psi.gif)
![E* E*](_em1.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | euexex 2088 |
Existential uniqueness and "at most one" double quantification.
(Contributed by Jim Kingdon, 28-Dec-2018.)
|
![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![ps ps](_psi.gif)
![E* E*](_em1.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 2moex 2089 |
Double quantification with "at most one." (Contributed by NM,
3-Dec-2001.)
|
![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif)
![A. A.](forall.gif) ![y y](_y.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | 2euex 2090 |
Double quantification with existential uniqueness. (Contributed by NM,
3-Dec-2001.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif)
![E. E.](exists.gif) ![y y](_y.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | 2eumo 2091 |
Double quantification with existential uniqueness and "at most one."
(Contributed by NM, 3-Dec-2001.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif)
![E* E*](_em1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | 2eu2ex 2092 |
Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | 2moswapdc 2093 |
A condition allowing swap of "at most one" and existential
quantifiers.
(Contributed by Jim Kingdon, 6-Jul-2018.)
|
DECID ![E.
E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 2euswapdc 2094 |
A condition allowing swap of uniqueness and existential quantifiers.
(Contributed by Jim Kingdon, 7-Jul-2018.)
|
DECID ![E.
E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![E* E*](_em1.gif) ![y y](_y.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 2exeu 2095 |
Double existential uniqueness implies double unique existential
quantification. (Contributed by NM, 3-Dec-2001.)
|
![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
|
Theorem | 2eu4 2096* |
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 ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) .
See 2exeu 2095 for a one-way implication. (Contributed by
NM,
3-Dec-2001.)
|
![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![w w](_w.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![(
(](lp.gif)
![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 2eu7 2097 |
Two equivalent expressions for double existential uniqueness.
(Contributed by NM, 19-Feb-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![E! E!](_e1.gif) ![y y](_y.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | euequ1 2098* |
Equality has existential uniqueness. (Contributed by Stefan Allan,
4-Dec-2008.)
|
![E!
E!](_e1.gif) ![y y](_y.gif) |
|
Theorem | exists1 2099* |
Two ways to express "only one thing exists." The left-hand side
requires only one variable to express this. Both sides are false in set
theory. (Contributed by NM, 5-Apr-2004.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![) )](rp.gif) |
|
Theorem | exists2 2100 |
A condition implying that at least two things exist. (Contributed by
NM, 10-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif)
![E! E!](_e1.gif)
![x x](_x.gif) ![) )](rp.gif) |