Theorem List for Intuitionistic Logic Explorer - 3601-3700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | snid 3601 |
A set is a member of its singleton. Part of Theorem 7.6 of [Quine]
p. 49. (Contributed by NM, 31-Dec-1993.)
|
|
|
Theorem | vsnid 3602 |
A setvar variable is a member of its singleton (common case).
(Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | elsn2g 3603 |
There is only one element in a singleton. Exercise 2 of [TakeutiZaring]
p. 15. This variation requires only that , rather than , be a
set. (Contributed by NM, 28-Oct-2003.)
|
|
|
Theorem | elsn2 3604 |
There is only one element in a singleton. Exercise 2 of [TakeutiZaring]
p. 15. This variation requires only that , rather than , be
a set. (Contributed by NM, 12-Jun-1994.)
|
|
|
Theorem | nelsn 3605 |
If a class is not equal to the class in a singleton, then it is not in the
singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof
shortened by BJ, 4-May-2021.)
|
|
|
Theorem | mosn 3606* |
A singleton has at most one element. This works whether is a
proper class or not, and in that sense can be seen as encompassing both
snmg 3688 and snprc 3635. (Contributed by Jim Kingdon,
30-Aug-2018.)
|
|
|
Theorem | ralsnsg 3607* |
Substitution expressed in terms of quantification over a singleton.
(Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2015.)
|
|
|
Theorem | ralsns 3608* |
Substitution expressed in terms of quantification over a singleton.
(Contributed by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | rexsns 3609* |
Restricted existential quantification over a singleton. (Contributed by
Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.)
|
|
|
Theorem | ralsng 3610* |
Substitution expressed in terms of quantification over a singleton.
(Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2015.)
|
|
|
Theorem | rexsng 3611* |
Restricted existential quantification over a singleton. (Contributed by
NM, 29-Jan-2012.)
|
|
|
Theorem | exsnrex 3612 |
There is a set being the element of a singleton if and only if there is an
element of the singleton. (Contributed by Alexander van der Vekens,
1-Jan-2018.)
|
|
|
Theorem | ralsn 3613* |
Convert a quantification over a singleton to a substitution.
(Contributed by NM, 27-Apr-2009.)
|
|
|
Theorem | rexsn 3614* |
Restricted existential quantification over a singleton. (Contributed by
Jeff Madsen, 5-Jan-2011.)
|
|
|
Theorem | eltpg 3615 |
Members of an unordered triple of classes. (Contributed by FL,
2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
|
|
|
Theorem | eldiftp 3616 |
Membership in a set with three elements removed. Similar to eldifsn 3697 and
eldifpr 3597. (Contributed by David A. Wheeler,
22-Jul-2017.)
|
|
|
Theorem | eltpi 3617 |
A member of an unordered triple of classes is one of them. (Contributed
by Mario Carneiro, 11-Feb-2015.)
|
|
|
Theorem | eltp 3618 |
A member of an unordered triple of classes is one of them. Special case
of Exercise 1 of [TakeutiZaring]
p. 17. (Contributed by NM,
8-Apr-1994.) (Revised by Mario Carneiro, 11-Feb-2015.)
|
|
|
Theorem | dftp2 3619* |
Alternate definition of unordered triple of classes. Special case of
Definition 5.3 of [TakeutiZaring]
p. 16. (Contributed by NM,
8-Apr-1994.)
|
|
|
Theorem | nfpr 3620 |
Bound-variable hypothesis builder for unordered pairs. (Contributed by
NM, 14-Nov-1995.)
|
|
|
Theorem | ralprg 3621* |
Convert a quantification over a pair to a conjunction. (Contributed by
NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | rexprg 3622* |
Convert a quantification over a pair to a disjunction. (Contributed by
NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | raltpg 3623* |
Convert a quantification over a triple to a conjunction. (Contributed
by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | rextpg 3624* |
Convert a quantification over a triple to a disjunction. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | ralpr 3625* |
Convert a quantification over a pair to a conjunction. (Contributed by
NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | rexpr 3626* |
Convert an existential quantification over a pair to a disjunction.
(Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro,
23-Apr-2015.)
|
|
|
Theorem | raltp 3627* |
Convert a quantification over a triple to a conjunction. (Contributed
by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | rextp 3628* |
Convert a quantification over a triple to a disjunction. (Contributed
by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | sbcsng 3629* |
Substitution expressed in terms of quantification over a singleton.
(Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2015.)
|
|
|
Theorem | nfsn 3630 |
Bound-variable hypothesis builder for singletons. (Contributed by NM,
14-Nov-1995.)
|
|
|
Theorem | csbsng 3631 |
Distribute proper substitution through the singleton of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
|
|
Theorem | disjsn 3632 |
Intersection with the singleton of a non-member is disjoint.
(Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon,
29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
|
|
|
Theorem | disjsn2 3633 |
Intersection of distinct singletons is disjoint. (Contributed by NM,
25-May-1998.)
|
|
|
Theorem | disjpr2 3634 |
The intersection of distinct unordered pairs is disjoint. (Contributed by
Alexander van der Vekens, 11-Nov-2017.)
|
|
|
Theorem | snprc 3635 |
The singleton of a proper class (one that doesn't exist) is the empty
set. Theorem 7.2 of [Quine] p. 48.
(Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | r19.12sn 3636* |
Special case of r19.12 2570 where its converse holds. (Contributed by
NM,
19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by
BJ, 20-Dec-2021.)
|
|
|
Theorem | rabsn 3637* |
Condition where a restricted class abstraction is a singleton.
(Contributed by NM, 28-May-2006.)
|
|
|
Theorem | rabrsndc 3638* |
A class abstraction over a decidable proposition restricted to a
singleton is either the empty set or the singleton itself. (Contributed
by Jim Kingdon, 8-Aug-2018.)
|
DECID
|
|
Theorem | euabsn2 3639* |
Another way to express existential uniqueness of a wff: its class
abstraction is a singleton. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
|
|
Theorem | euabsn 3640 |
Another way to express existential uniqueness of a wff: its class
abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
|
|
|
Theorem | reusn 3641* |
A way to express restricted existential uniqueness of a wff: its
restricted class abstraction is a singleton. (Contributed by NM,
30-May-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|
|
|
Theorem | absneu 3642 |
Restricted existential uniqueness determined by a singleton.
(Contributed by NM, 29-May-2006.)
|
|
|
Theorem | rabsneu 3643 |
Restricted existential uniqueness determined by a singleton.
(Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro,
23-Dec-2016.)
|
|
|
Theorem | eusn 3644* |
Two ways to express " is a singleton." (Contributed by NM,
30-Oct-2010.)
|
|
|
Theorem | rabsnt 3645* |
Truth implied by equality of a restricted class abstraction and a
singleton. (Contributed by NM, 29-May-2006.) (Proof shortened by Mario
Carneiro, 23-Dec-2016.)
|
|
|
Theorem | prcom 3646 |
Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | preq1 3647 |
Equality theorem for unordered pairs. (Contributed by NM,
29-Mar-1998.)
|
|
|
Theorem | preq2 3648 |
Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | preq12 3649 |
Equality theorem for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq1i 3650 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq2i 3651 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq12i 3652 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq1d 3653 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq2d 3654 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq12d 3655 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | tpeq1 3656 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
|
|
Theorem | tpeq2 3657 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
|
|
Theorem | tpeq3 3658 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
|
|
Theorem | tpeq1d 3659 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tpeq2d 3660 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tpeq3d 3661 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tpeq123d 3662 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tprot 3663 |
Rotation of the elements of an unordered triple. (Contributed by Alan
Sare, 24-Oct-2011.)
|
|
|
Theorem | tpcoma 3664 |
Swap 1st and 2nd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
|
|
Theorem | tpcomb 3665 |
Swap 2nd and 3rd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
|
|
Theorem | tpass 3666 |
Split off the first element of an unordered triple. (Contributed by Mario
Carneiro, 5-Jan-2016.)
|
|
|
Theorem | qdass 3667 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
|
|
Theorem | qdassr 3668 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
|
|
Theorem | tpidm12 3669 |
Unordered triple is just
an overlong way to write
.
(Contributed by David A. Wheeler, 10-May-2015.)
|
|
|
Theorem | tpidm13 3670 |
Unordered triple is just
an overlong way to write
.
(Contributed by David A. Wheeler, 10-May-2015.)
|
|
|
Theorem | tpidm23 3671 |
Unordered triple is just
an overlong way to write
.
(Contributed by David A. Wheeler, 10-May-2015.)
|
|
|
Theorem | tpidm 3672 |
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler,
10-May-2015.)
|
|
|
Theorem | tppreq3 3673 |
An unordered triple is an unordered pair if one of its elements is
identical with another element. (Contributed by Alexander van der Vekens,
6-Oct-2017.)
|
|
|
Theorem | prid1g 3674 |
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by Stefan
Allan, 8-Nov-2008.)
|
|
|
Theorem | prid2g 3675 |
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by Stefan
Allan, 8-Nov-2008.)
|
|
|
Theorem | prid1 3676 |
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | prid2 3677 |
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | prprc1 3678 |
A proper class vanishes in an unordered pair. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | prprc2 3679 |
A proper class vanishes in an unordered pair. (Contributed by NM,
22-Mar-2006.)
|
|
|
Theorem | prprc 3680 |
An unordered pair containing two proper classes is the empty set.
(Contributed by NM, 22-Mar-2006.)
|
|
|
Theorem | tpid1 3681 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | tpid1g 3682 |
Closed theorem form of tpid1 3681. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
|
|
Theorem | tpid2 3683 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | tpid2g 3684 |
Closed theorem form of tpid2 3683. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
|
|
Theorem | tpid3g 3685 |
Closed theorem form of tpid3 3686. (Contributed by Alan Sare,
24-Oct-2011.)
|
|
|
Theorem | tpid3 3686 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | snnzg 3687 |
The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|
|
|
Theorem | snmg 3688* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
|
|
Theorem | snnz 3689 |
The singleton of a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | snm 3690* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
|
|
Theorem | prmg 3691* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
|
|
Theorem | prnz 3692 |
A pair containing a set is not empty. (Contributed by NM,
9-Apr-1994.)
|
|
|
Theorem | prm 3693* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
|
|
Theorem | prnzg 3694 |
A pair containing a set is not empty. (Contributed by FL,
19-Sep-2011.)
|
|
|
Theorem | tpnz 3695 |
A triplet containing a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | snss 3696 |
The singleton of an element of a class is a subset of the class.
Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | eldifsn 3697 |
Membership in a set with an element removed. (Contributed by NM,
10-Oct-2007.)
|
|
|
Theorem | ssdifsn 3698 |
Subset of a set with an element removed. (Contributed by Emmett Weisz,
7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
|
|
|
Theorem | eldifsni 3699 |
Membership in a set with an element removed. (Contributed by NM,
10-Mar-2015.)
|
|
|
Theorem | neldifsn 3700 |
is not in . (Contributed by David Moews,
1-May-2017.)
|
|