Type  Label  Description 
Statement 

Theorem  preq12 3801 
Equality theorem for unordered pairs. (Contributed by NM,
19Oct2012.)



Theorem  preq1i 3802 
Equality inference for unordered pairs. (Contributed by NM,
19Oct2012.)



Theorem  preq2i 3803 
Equality inference for unordered pairs. (Contributed by NM,
19Oct2012.)



Theorem  preq12i 3804 
Equality inference for unordered pairs. (Contributed by NM,
19Oct2012.)



Theorem  preq1d 3805 
Equality deduction for unordered pairs. (Contributed by NM,
19Oct2012.)



Theorem  preq2d 3806 
Equality deduction for unordered pairs. (Contributed by NM,
19Oct2012.)



Theorem  preq12d 3807 
Equality deduction for unordered pairs. (Contributed by NM,
19Oct2012.)



Theorem  tpeq1 3808 
Equality theorem for unordered triples. (Contributed by NM,
13Sep2011.)



Theorem  tpeq2 3809 
Equality theorem for unordered triples. (Contributed by NM,
13Sep2011.)



Theorem  tpeq3 3810 
Equality theorem for unordered triples. (Contributed by NM,
13Sep2011.)



Theorem  tpeq1d 3811 
Equality theorem for unordered triples. (Contributed by NM,
22Jun2014.)



Theorem  tpeq2d 3812 
Equality theorem for unordered triples. (Contributed by NM,
22Jun2014.)



Theorem  tpeq3d 3813 
Equality theorem for unordered triples. (Contributed by NM,
22Jun2014.)



Theorem  tpeq123d 3814 
Equality theorem for unordered triples. (Contributed by NM,
22Jun2014.)



Theorem  tprot 3815 
Rotation of the elements of an unordered triple. (Contributed by Alan
Sare, 24Oct2011.)



Theorem  tpcoma 3816 
Swap 1st and 2nd members of an undordered triple. (Contributed by NM,
22May2015.)



Theorem  tpcomb 3817 
Swap 2nd and 3rd members of an undordered triple. (Contributed by NM,
22May2015.)



Theorem  tpass 3818 
Split off the first element of an unordered triple. (Contributed by Mario
Carneiro, 5Jan2016.)



Theorem  qdass 3819 
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5Jan2016.)



Theorem  qdassr 3820 
Two ways to write an unordered quadruple. (Contributed by Mario Carneiro,
5Jan2016.)



Theorem  tpidm12 3821 
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler, 10May2015.)



Theorem  tpidm13 3822 
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler, 10May2015.)



Theorem  tpidm23 3823 
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler, 10May2015.)



Theorem  tpidm 3824 
Unordered triple is just
an overlong way to write
. (Contributed by David A. Wheeler,
10May2015.)



Theorem  prid1g 3825 
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by Stefan
Allan, 8Nov2008.)



Theorem  prid2g 3826 
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by Stefan
Allan, 8Nov2008.)



Theorem  prid1 3827 
An unordered pair contains its first member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5Aug1993.)



Theorem  prid2 3828 
An unordered pair contains its second member. Part of Theorem 7.6 of
[Quine] p. 49. (Contributed by NM,
5Aug1993.)



Theorem  tpid1 3829 
One of the three elements of an unordered triple. (Contributed by NM,
7Apr1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)



Theorem  tpid2 3830 
One of the three elements of an unordered triple. (Contributed by NM,
7Apr1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)



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, 24Oct2011.)



Theorem  tpid3 3832 
One of the three elements of an unordered triple. (Contributed by NM,
7Apr1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)



Theorem  snnzg 3833 
The singleton of a set is not empty. (Contributed by NM, 14Dec2008.)



Theorem  snnz 3834 
The singleton of a set is not empty. (Contributed by NM,
10Apr1994.)



Theorem  prnz 3835 
A pair containing a set is not empty. (Contributed by NM,
9Apr1994.)



Theorem  prnzg 3836 
A pair containing a set is not empty. (Contributed by FL,
19Sep2011.)



Theorem  tpnz 3837 
A triplet containing a set is not empty. (Contributed by NM,
10Apr1994.)



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, 5Aug1993.)



Theorem  eldifsn 3839 
Membership in a set with an element removed. (Contributed by NM,
10Oct2007.)



Theorem  eldifsni 3840 
Membership in a set with an element removed. (Contributed by NM,
10Mar2015.)



Theorem  neldifsn 3841 
is not in . (Contributed by David Moews,
1May2017.)



Theorem  neldifsnd 3842 
is not in . Deduction form. (Contributed by
David Moews, 1May2017.)



Theorem  rexdifsn 3843 
Restricted existential quantification over a set with an element removed.
(Contributed by NM, 4Feb2015.)



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, 22Jul2001.)



Theorem  difsn 3845 
An element not in a set can be removed without affecting the set.
(Contributed by NM, 16Mar2006.) (Proof shortened by Andrew Salmon,
29Jun2011.)



Theorem  difprsnss 3846 
Removal of a singleton from an unordered pair. (Contributed by NM,
16Mar2006.) (Proof shortened by Andrew Salmon, 29Jun2011.)



Theorem  difprsn1 3847 
Removal of a singleton from an unordered pair. (Contributed by Thierry
Arnoux, 4Feb2017.)



Theorem  difprsn2 3848 
Removal of a singleton from an unordered pair. (Contributed by Alexander
van der Vekens, 5Oct2017.)



Theorem  diftpsn3 3849 
Removal of a singleton from an unordered triple. (Contributed by
Alexander van der Vekens, 5Oct2017.)



Theorem  difsnb 3850 
equals if and only if is not a member of
.
Generalization of difsn 3845. (Contributed by David Moews,
1May2017.)



Theorem  difsnpss 3851 
is a proper subclass of
if and only if is a
member of .
(Contributed by David Moews, 1May2017.)



Theorem  snssi 3852 
The singleton of an element of a class is a subset of the class.
(Contributed by NM, 6Jun1994.)



Theorem  snssd 3853 
The singleton of an element of a class is a subset of the class
(deduction rule). (Contributed by Jonathan BenNaim, 3Jun2011.)



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, 2Oct2006.)



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, 7Aug1994.)



Theorem  snsspr1 3856 
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 27Aug2004.)



Theorem  snsspr2 3857 
A singleton is a subset of an unordered pair containing its member.
(Contributed by NM, 2May2009.)



Theorem  snsstp1 3858 
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9Oct2013.)



Theorem  snsstp2 3859 
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9Oct2013.)



Theorem  snsstp3 3860 
A singleton is a subset of an unordered triple containing its member.
(Contributed by NM, 9Oct2013.)



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,
30May1994.) (Proof shortened by
Andrew Salmon, 29Jun2011.)



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,
22Mar2006.) (Proof shortened by
Andrew Salmon, 29Jun2011.)



Theorem  prssi 3863 
A pair of elements of a class is a subset of the class. (Contributed by
NM, 16Jan2015.)



Theorem  sssn 3864 
The subsets of a singleton. (Contributed by NM, 24Apr2004.)



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, 2Jul2016.)



Theorem  ssunsn 3866 
Possible values for a set sandwiched between another set and it plus a
singleton. (Contributed by Mario Carneiro, 2Jul2016.)



Theorem  eqsn 3867* 
Two ways to express that a nonempty set equals a singleton.
(Contributed by NM, 15Dec2007.)



Theorem  ssunpr 3868 
Possible values for a set sandwiched between another set and it plus a
singleton. (Contributed by Mario Carneiro, 2Jul2016.)



Theorem  sspr 3869 
The subsets of a pair. (Contributed by NM, 16Mar2006.) (Proof
shortened by Mario Carneiro, 2Jul2016.)



Theorem  sstp 3870 
The subsets of a triple. (Contributed by Mario Carneiro, 2Jul2016.)



Theorem  tpss 3871 
A triplet of elements of a class is a subset of the class. (Contributed
by NM, 9Apr1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)



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,
27Aug1993.)



Theorem  snsssn 3873 
If a singleton is a subset of another, their members are equal.
(Contributed by NM, 28May2006.)



Theorem  sneqrg 3874 
Closed form of sneqr 3872. (Contributed by Scott Fenton, 1Apr2011.)



Theorem  sneqbg 3875 
Two singletons of sets are equal iff their elements are equal.
(Contributed by Scott Fenton, 16Apr2012.)



Theorem  sneqb 3876 
Biconditional equality for singletons. (Contributed by SF,
14Jan2015.)



Theorem  snsspw 3877 
The singleton of a class is a subset of its power class. (Contributed
by NM, 5Aug1993.)



Theorem  prsspw 3878 
An unordered pair belongs to the power class of a class iff each member
belongs to the class. (Contributed by NM, 10Dec2003.) (Proof
shortened by Andrew Salmon, 26Jun2011.)



Theorem  ralunsn 3879* 
Restricted quantification over the union of a set and a singleton, using
implicit substitution. (Contributed by Paul Chapman, 17Nov2012.)
(Revised by Mario Carneiro, 23Apr2015.)



Theorem  2ralunsn 3880* 
Double restricted quantification over the union of a set and a
singleton, using implicit substitution. (Contributed by Paul Chapman,
17Nov2012.)



Theorem  pwsn 3881 
The power set of a singleton. (Contributed by NM, 5Jun2006.)



Theorem  pwsnALT 3882 
The power set of a singleton (direct proof). TO DO  should we keep
this? (Contributed by NM, 5Jun2006.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  pwpr 3883 
The power set of an unordered pair. (Contributed by NM, 1May2009.)



Theorem  pwtp 3884 
The power set of an unordered triple. (Contributed by Mario Carneiro,
2Jul2016.)



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, 2May2009.)



Theorem  pwv 3886 
The power class of the universe is the universe. Exercise 4.12(d) of
[Mendelson] p. 235. (Contributed by NM,
14Sep2003.)



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,
15Jan2015.)



Theorem  dfpss4 3888* 
Alternate definition of proper subset. Theorem IX.4.21 of [Rosser]
p. 236. (Contributed by SF, 19Jan2015.)



Theorem  adj11 3889 
Adjoining a new element is onetoone. (Contributed by SF,
29Jan2015.)



Theorem  disj5 3890 
Two ways of saying that two classes are disjoint. (Contributed by SF,
5Feb2015.)

∼ 

2.1.17 The union of a class


Syntax  cuni 3891 
Extend class notation to include the union of a class (read: 'union
')



Definition  dfuni 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
(exuni in set.mm). This is similar to the union of two classes
dfun 3214. (Contributed by NM, 23Aug1993.)



Theorem  dfuni2 3893* 
Alternate definition of class union. (Contributed by NM,
28Jun1998.)



Theorem  eluni 3894* 
Membership in class union. (Contributed by NM, 22May1994.)



Theorem  eluni2 3895* 
Membership in class union. Restricted quantifier version. (Contributed
by NM, 31Aug1999.)



Theorem  elunii 3896 
Membership in class union. (Contributed by NM, 24Mar1995.)



Theorem  nfuni 3897 
Boundvariable hypothesis builder for union. (Contributed by NM,
30Dec1996.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  nfunid 3898 
Deduction version of nfuni 3897. (Contributed by NM, 18Feb2013.)



Theorem  csbunig 3899 
Distribute proper substitution through the union of a class.
(Contributed by Alan Sare, 10Nov2012.)



Theorem  unieq 3900 
Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18.
(Contributed by NM, 10Aug1993.) (Proof shortened by Andrew Salmon,
29Jun2011.)

