Theorem List for New Foundations Explorer - 3801-3900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | preq12 3801 |
Equality theorem for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq1i 3802 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq2i 3803 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq12i 3804 |
Equality inference for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq1d 3805 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq2d 3806 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | preq12d 3807 |
Equality deduction for unordered pairs. (Contributed by NM,
19-Oct-2012.)
|
|
|
Theorem | tpeq1 3808 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
|
|
Theorem | tpeq2 3809 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
|
|
Theorem | tpeq3 3810 |
Equality theorem for unordered triples. (Contributed by NM,
13-Sep-2011.)
|
|
|
Theorem | tpeq1d 3811 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tpeq2d 3812 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tpeq3d 3813 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tpeq123d 3814 |
Equality theorem for unordered triples. (Contributed by NM,
22-Jun-2014.)
|
|
|
Theorem | tprot 3815 |
Rotation of the elements of an unordered triple. (Contributed by Alan
Sare, 24-Oct-2011.)
|
|
|
Theorem | tpcoma 3816 |
Swap 1st and 2nd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
|
|
Theorem | tpcomb 3817 |
Swap 2nd and 3rd members of an undordered triple. (Contributed by NM,
22-May-2015.)
|
|
|
Theorem | tpass 3818 |
Split off the first element of an unordered triple. (Contributed by Mario
Carneiro, 5-Jan-2016.)
|
|
|
Theorem | qdass 3819 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
|
|
Theorem | qdassr 3820 |
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
|
|
Theorem | tpidm12 3821 |
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler, 10-May-2015.)
|
|
|
Theorem | tpidm13 3822 |
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler, 10-May-2015.)
|
|
|
Theorem | tpidm23 3823 |
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler, 10-May-2015.)
|
|
|
Theorem | tpidm 3824 |
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler,
10-May-2015.)
|
|
|
Theorem | prid1g 3825 |
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 3826 |
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 3827 |
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | prid2 3828 |
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | tpid1 3829 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | tpid2 3830 |
One of the three elements of an unordered triple. (Contributed by NM,
7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | tpid3g 3831 |
Closed theorem form of tpid3 3832. This proof was automatically generated
from the virtual deduction proof tpid3gVD in set.mm using a translation
program. (Contributed by Alan Sare, 24-Oct-2011.)
|
|
|
Theorem | tpid3 3832 |
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 3833 |
The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|
|
|
Theorem | snnz 3834 |
The singleton of a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | prnz 3835 |
A pair containing a set is not empty. (Contributed by NM,
9-Apr-1994.)
|
|
|
Theorem | prnzg 3836 |
A pair containing a set is not empty. (Contributed by FL,
19-Sep-2011.)
|
|
|
Theorem | tpnz 3837 |
A triplet containing a set is not empty. (Contributed by NM,
10-Apr-1994.)
|
|
|
Theorem | snss 3838 |
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 3839 |
Membership in a set with an element removed. (Contributed by NM,
10-Oct-2007.)
|
|
|
Theorem | eldifsni 3840 |
Membership in a set with an element removed. (Contributed by NM,
10-Mar-2015.)
|
|
|
Theorem | neldifsn 3841 |
is not in . (Contributed by David Moews,
1-May-2017.)
|
|
|
Theorem | neldifsnd 3842 |
is not in . Deduction form. (Contributed by
David Moews, 1-May-2017.)
|
|
|
Theorem | rexdifsn 3843 |
Restricted existential quantification over a set with an element removed.
(Contributed by NM, 4-Feb-2015.)
|
|
|
Theorem | snssg 3844 |
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 3845 |
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 3846 |
Removal of a singleton from an unordered pair. (Contributed by NM,
16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
|
|
Theorem | difprsn1 3847 |
Removal of a singleton from an unordered pair. (Contributed by Thierry
Arnoux, 4-Feb-2017.)
|
|
|
Theorem | difprsn2 3848 |
Removal of a singleton from an unordered pair. (Contributed by Alexander
van der Vekens, 5-Oct-2017.)
|
|
|
Theorem | diftpsn3 3849 |
Removal of a singleton from an unordered triple. (Contributed by
Alexander van der Vekens, 5-Oct-2017.)
|
|
|
Theorem | difsnb 3850 |
equals if and only if is not a member of
.
Generalization of difsn 3845. (Contributed by David Moews,
1-May-2017.)
|
|
|
Theorem | difsnpss 3851 |
is a proper subclass of
if and only if is a
member of .
(Contributed by David Moews, 1-May-2017.)
|
|
|
Theorem | snssi 3852 |
The singleton of an element of a class is a subset of the class.
(Contributed by NM, 6-Jun-1994.)
|
|
|
Theorem | snssd 3853 |
The singleton of an element of a class is a subset of the class
(deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | difsnid 3854 |
If we remove a single element from a class then put it back in, we end up
with the original class. (Contributed by NM, 2-Oct-2006.)
|
|
|
Theorem | pwpw0 3855 |
Compute the power set of the power set of the empty set. (See pw0 4160
for
the power set of the empty set.) Theorem 90 of [Suppes] p. 48.
Although this theorem is a special case of pwsn 3881,
we have chosen to
show a direct elementary proof. (Contributed by NM, 7-Aug-1994.)
|
|
|
Theorem | snsspr1 3856 |
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 27-Aug-2004.)
|
|
|
Theorem | snsspr2 3857 |
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 2-May-2009.)
|
|
|
Theorem | snsstp1 3858 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
|
|
Theorem | snsstp2 3859 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
|
|
Theorem | snsstp3 3860 |
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9-Oct-2013.)
|
|
|
Theorem | prss 3861 |
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 3862 |
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 3863 |
A pair of elements of a class is a subset of the class. (Contributed by
NM, 16-Jan-2015.)
|
|
|
Theorem | sssn 3864 |
The subsets of a singleton. (Contributed by NM, 24-Apr-2004.)
|
|
|
Theorem | ssunsn2 3865 |
The property of being sandwiched between two sets naturally splits under
union with a singleton. This is the induction hypothesis for the
determination of large powersets such as pwtp 3884.
(Contributed by Mario
Carneiro, 2-Jul-2016.)
|
|
|
Theorem | ssunsn 3866 |
Possible values for a set sandwiched between another set and it plus a
singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
|
|
|
Theorem | eqsn 3867* |
Two ways to express that a nonempty set equals a singleton.
(Contributed by NM, 15-Dec-2007.)
|
|
|
Theorem | ssunpr 3868 |
Possible values for a set sandwiched between another set and it plus a
singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
|
|
|
Theorem | sspr 3869 |
The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof
shortened by Mario Carneiro, 2-Jul-2016.)
|
|
|
Theorem | sstp 3870 |
The subsets of a triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
|
|
|
Theorem | tpss 3871 |
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 | sneqr 3872 |
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 3873 |
If a singleton is a subset of another, their members are equal.
(Contributed by NM, 28-May-2006.)
|
|
|
Theorem | sneqrg 3874 |
Closed form of sneqr 3872. (Contributed by Scott Fenton, 1-Apr-2011.)
|
|
|
Theorem | sneqbg 3875 |
Two singletons of sets are equal iff their elements are equal.
(Contributed by Scott Fenton, 16-Apr-2012.)
|
|
|
Theorem | sneqb 3876 |
Biconditional equality for singletons. (Contributed by SF,
14-Jan-2015.)
|
|
|
Theorem | snsspw 3877 |
The singleton of a class is a subset of its power class. (Contributed
by NM, 5-Aug-1993.)
|
|
|
Theorem | prsspw 3878 |
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 | ralunsn 3879* |
Restricted quantification over the union of a set and a singleton, using
implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
(Revised by Mario Carneiro, 23-Apr-2015.)
|
|
|
Theorem | 2ralunsn 3880* |
Double restricted quantification over the union of a set and a
singleton, using implicit substitution. (Contributed by Paul Chapman,
17-Nov-2012.)
|
|
|
Theorem | pwsn 3881 |
The power set of a singleton. (Contributed by NM, 5-Jun-2006.)
|
|
|
Theorem | pwsnALT 3882 |
The power set of a singleton (direct proof). TO DO - should we keep
this? (Contributed by NM, 5-Jun-2006.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | pwpr 3883 |
The power set of an unordered pair. (Contributed by NM, 1-May-2009.)
|
|
|
Theorem | pwtp 3884 |
The power set of an unordered triple. (Contributed by Mario Carneiro,
2-Jul-2016.)
|
|
|
Theorem | pwpwpw0 3885 |
Compute the power set of the power set of the power set of the empty set.
(See also pw0 4160 and pwpw0 3855.) (Contributed by NM, 2-May-2009.)
|
|
|
Theorem | pwv 3886 |
The power class of the universe is the universe. Exercise 4.12(d) of
[Mendelson] p. 235. (Contributed by NM,
14-Sep-2003.)
|
|
|
Theorem | unsneqsn 3887 |
If union with a singleton yields a singleton, then the first argument is
either also the singleton or is the empty set. (Contributed by SF,
15-Jan-2015.)
|
|
|
Theorem | dfpss4 3888* |
Alternate definition of proper subset. Theorem IX.4.21 of [Rosser]
p. 236. (Contributed by SF, 19-Jan-2015.)
|
|
|
Theorem | adj11 3889 |
Adjoining a new element is one-to-one. (Contributed by SF,
29-Jan-2015.)
|
|
|
Theorem | disj5 3890 |
Two ways of saying that two classes are disjoint. (Contributed by SF,
5-Feb-2015.)
|
∼ |
|
2.1.17 The union of a class
|
|
Syntax | cuni 3891 |
Extend class notation to include the union of a class (read: 'union
')
|
|
|
Definition | df-uni 3892* |
Define the union of a class i.e. the collection of all members of the
members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For
example, 1 , 3 1 , 8 1 , 3 , 8
(ex-uni in set.mm). This is similar to the union of two classes
df-un 3214. (Contributed by NM, 23-Aug-1993.)
|
|
|
Theorem | dfuni2 3893* |
Alternate definition of class union. (Contributed by NM,
28-Jun-1998.)
|
|
|
Theorem | eluni 3894* |
Membership in class union. (Contributed by NM, 22-May-1994.)
|
|
|
Theorem | eluni2 3895* |
Membership in class union. Restricted quantifier version. (Contributed
by NM, 31-Aug-1999.)
|
|
|
Theorem | elunii 3896 |
Membership in class union. (Contributed by NM, 24-Mar-1995.)
|
|
|
Theorem | nfuni 3897 |
Bound-variable hypothesis builder for union. (Contributed by NM,
30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | nfunid 3898 |
Deduction version of nfuni 3897. (Contributed by NM, 18-Feb-2013.)
|
|
|
Theorem | csbunig 3899 |
Distribute proper substitution through the union of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
|
|
Theorem | unieq 3900 |
Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18.
(Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
|