Theorem List for Intuitionistic Logic Explorer - 3601-3700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | preq2 3601 |
Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | preq12 3602 |
Equality theorem for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq1i 3603 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq2i 3604 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq12i 3605 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq1d 3606 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq2d 3607 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq12d 3608 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | tpeq1 3609 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
|
|
Theorem | tpeq2 3610 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
|
|
Theorem | tpeq3 3611 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
|
|
Theorem | tpeq1d 3612 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tpeq2d 3613 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tpeq3d 3614 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tpeq123d 3615 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tprot 3616 |
Rotation of the elements of an unordered triple. (Contributed by Alan
Sare, 24-Oct-2011.)
|
|
|
Theorem | tpcoma 3617 |
Swap 1st and 2nd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
|
|
Theorem | tpcomb 3618 |
Swap 2nd and 3rd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
|
|
Theorem | tpass 3619 |
Split off the first element of an unordered triple. (Contributed by Mario
Carneiro, 5-Jan-2016.)
|
|
|
Theorem | qdass 3620 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
|
|
Theorem | qdassr 3621 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
|
|
Theorem | tpidm12 3622 |
Unordered triple is just
an overlong way to write
.
(Contributed by David A. Wheeler, 10-May-2015.)
|
|
|
Theorem | tpidm13 3623 |
Unordered triple is just
an overlong way to write
.
(Contributed by David A. Wheeler, 10-May-2015.)
|
|
|
Theorem | tpidm23 3624 |
Unordered triple is just
an overlong way to write
.
(Contributed by David A. Wheeler, 10-May-2015.)
|
|
|
Theorem | tpidm 3625 |
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler,
10-May-2015.)
|
|
|
Theorem | tppreq3 3626 |
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 3627 |
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 3628 |
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 3629 |
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | prid2 3630 |
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | prprc1 3631 |
A proper class vanishes in an unordered pair. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | prprc2 3632 |
A proper class vanishes in an unordered pair. (Contributed by NM,
22-Mar-2006.)
|
|
|
Theorem | prprc 3633 |
An unordered pair containing two proper classes is the empty set.
(Contributed by NM, 22-Mar-2006.)
|
|
|
Theorem | tpid1 3634 |
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 3635 |
Closed theorem form of tpid1 3634. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
|
|
Theorem | tpid2 3636 |
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 3637 |
Closed theorem form of tpid2 3636. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
|
|
Theorem | tpid3g 3638 |
Closed theorem form of tpid3 3639. (Contributed by Alan Sare,
24-Oct-2011.)
|
|
|
Theorem | tpid3 3639 |
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 3640 |
The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|
|
|
Theorem | snmg 3641* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
|
|
Theorem | snnz 3642 |
The singleton of a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | snm 3643* |
The singleton of a set is inhabited. (Contributed by Jim Kingdon,
11-Aug-2018.)
|
|
|
Theorem | prmg 3644* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
|
|
Theorem | prnz 3645 |
A pair containing a set is not empty. (Contributed by NM,
9-Apr-1994.)
|
|
|
Theorem | prm 3646* |
A pair containing a set is inhabited. (Contributed by Jim Kingdon,
21-Sep-2018.)
|
|
|
Theorem | prnzg 3647 |
A pair containing a set is not empty. (Contributed by FL,
19-Sep-2011.)
|
|
|
Theorem | tpnz 3648 |
A triplet containing a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | snss 3649 |
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 3650 |
Membership in a set with an element removed. (Contributed by NM,
10-Oct-2007.)
|
|
|
Theorem | ssdifsn 3651 |
Subset of a set with an element removed. (Contributed by Emmett Weisz,
7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
|
|
|
Theorem | eldifsni 3652 |
Membership in a set with an element removed. (Contributed by NM,
10-Mar-2015.)
|
|
|
Theorem | neldifsn 3653 |
is not in . (Contributed by David Moews,
1-May-2017.)
|
|
|
Theorem | neldifsnd 3654 |
is not in . Deduction form. (Contributed by
David Moews, 1-May-2017.)
|
|
|
Theorem | rexdifsn 3655 |
Restricted existential quantification over a set with an element removed.
(Contributed by NM, 4-Feb-2015.)
|
|
|
Theorem | snssg 3656 |
The singleton of an element of a class is a subset of the class.
Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 22-Jul-2001.)
|
|
|
Theorem | difsn 3657 |
An element not in a set can be removed without affecting the set.
(Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
|
|
Theorem | difprsnss 3658 |
Removal of a singleton from an unordered pair. (Contributed by NM,
16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | difprsn1 3659 |
Removal of a singleton from an unordered pair. (Contributed by Thierry
Arnoux, 4-Feb-2017.)
|
|
|
Theorem | difprsn2 3660 |
Removal of a singleton from an unordered pair. (Contributed by Alexander
van der Vekens, 5-Oct-2017.)
|
|
|
Theorem | diftpsn3 3661 |
Removal of a singleton from an unordered triple. (Contributed by
Alexander van der Vekens, 5-Oct-2017.)
|
|
|
Theorem | difpr 3662 |
Removing two elements as pair of elements corresponds to removing each of
the two elements as singletons. (Contributed by Alexander van der Vekens,
13-Jul-2018.)
|
|
|
Theorem | difsnb 3663 |
equals if and only if is not a member of
. Generalization
of difsn 3657. (Contributed by David Moews,
1-May-2017.)
|
|
|
Theorem | snssi 3664 |
The singleton of an element of a class is a subset of the class.
(Contributed by NM, 6-Jun-1994.)
|
|
|
Theorem | snssd 3665 |
The singleton of an element of a class is a subset of the class
(deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | difsnss 3666 |
If we remove a single element from a class then put it back in, we end up
with a subset of the original class. If equality is decidable, we can
replace subset with equality as seen in nndifsnid 6403. (Contributed by Jim
Kingdon, 10-Aug-2018.)
|
|
|
Theorem | pw0 3667 |
Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
|
|
Theorem | snsspr1 3668 |
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 27-Aug-2004.)
|
|
|
Theorem | snsspr2 3669 |
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 2-May-2009.)
|
|
|
Theorem | snsstp1 3670 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
|
|
Theorem | snsstp2 3671 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
|
|
Theorem | snsstp3 3672 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
|
|
Theorem | prsstp12 3673 |
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | prsstp13 3674 |
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | prsstp23 3675 |
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | prss 3676 |
A pair of elements of a class is a subset of the class. Theorem 7.5 of
[Quine] p. 49. (Contributed by NM,
30-May-1994.) (Proof shortened by
Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | prssg 3677 |
A pair of elements of a class is a subset of the class. Theorem 7.5 of
[Quine] p. 49. (Contributed by NM,
22-Mar-2006.) (Proof shortened by
Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | prssi 3678 |
A pair of elements of a class is a subset of the class. (Contributed by
NM, 16-Jan-2015.)
|
|
|
Theorem | prsspwg 3679 |
An unordered pair belongs to the power class of a class iff each member
belongs to the class. (Contributed by Thierry Arnoux, 3-Oct-2016.)
(Revised by NM, 18-Jan-2018.)
|
|
|
Theorem | sssnr 3680 |
Empty set and the singleton itself are subsets of a singleton.
Concerning the converse, see exmidsssn 4125. (Contributed by Jim Kingdon,
10-Aug-2018.)
|
|
|
Theorem | sssnm 3681* |
The inhabited subset of a singleton. (Contributed by Jim Kingdon,
10-Aug-2018.)
|
|
|
Theorem | eqsnm 3682* |
Two ways to express that an inhabited set equals a singleton.
(Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | ssprr 3683 |
The subsets of a pair. (Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | sstpr 3684 |
The subsets of a triple. (Contributed by Jim Kingdon, 11-Aug-2018.)
|
|
|
Theorem | tpss 3685 |
A triplet of elements of a class is a subset of the class. (Contributed
by NM, 9-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | tpssi 3686 |
A triple of elements of a class is a subset of the class. (Contributed by
Alexander van der Vekens, 1-Feb-2018.)
|
|
|
Theorem | sneqr 3687 |
If the singletons of two sets are equal, the two sets are equal. Part
of Exercise 4 of [TakeutiZaring]
p. 15. (Contributed by NM,
27-Aug-1993.)
|
|
|
Theorem | snsssn 3688 |
If a singleton is a subset of another, their members are equal.
(Contributed by NM, 28-May-2006.)
|
|
|
Theorem | sneqrg 3689 |
Closed form of sneqr 3687. (Contributed by Scott Fenton, 1-Apr-2011.)
|
|
|
Theorem | sneqbg 3690 |
Two singletons of sets are equal iff their elements are equal.
(Contributed by Scott Fenton, 16-Apr-2012.)
|
|
|
Theorem | snsspw 3691 |
The singleton of a class is a subset of its power class. (Contributed
by NM, 5-Aug-1993.)
|
|
|
Theorem | prsspw 3692 |
An unordered pair belongs to the power class of a class iff each member
belongs to the class. (Contributed by NM, 10-Dec-2003.) (Proof
shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
Theorem | preqr1g 3693 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. Closed form of
preqr1 3695. (Contributed by Jim Kingdon, 21-Sep-2018.)
|
|
|
Theorem | preqr2g 3694 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the second elements are equal. Closed form of
preqr2 3696. (Contributed by Jim Kingdon, 21-Sep-2018.)
|
|
|
Theorem | preqr1 3695 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. (Contributed by
NM, 18-Oct-1995.)
|
|
|
Theorem | preqr2 3696 |
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same first element, the second elements are equal. (Contributed by
NM, 5-Aug-1993.)
|
|
|
Theorem | preq12b 3697 |
Equality relationship for two unordered pairs. (Contributed by NM,
17-Oct-1996.)
|
|
|
Theorem | prel12 3698 |
Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|
|
|
Theorem | opthpr 3699 |
A way to represent ordered pairs using unordered pairs with distinct
members. (Contributed by NM, 27-Mar-2007.)
|
|
|
Theorem | preq12bg 3700 |
Closed form of preq12b 3697. (Contributed by Scott Fenton,
28-Mar-2014.)
|
|