Type  Label  Description 
Statement 

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



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



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



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



Theorem  prsstp12 3705 
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11Aug2018.)



Theorem  prsstp13 3706 
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11Aug2018.)



Theorem  prsstp23 3707 
A pair is a subset of an unordered triple containing its members.
(Contributed by Jim Kingdon, 11Aug2018.)



Theorem  prss 3708 
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 3709 
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 3710 
A pair of elements of a class is a subset of the class. (Contributed by
NM, 16Jan2015.)



Theorem  prsspwg 3711 
An unordered pair belongs to the power class of a class iff each member
belongs to the class. (Contributed by Thierry Arnoux, 3Oct2016.)
(Revised by NM, 18Jan2018.)



Theorem  sssnr 3712 
Empty set and the singleton itself are subsets of a singleton.
Concerning the converse, see exmidsssn 4158. (Contributed by Jim Kingdon,
10Aug2018.)



Theorem  sssnm 3713* 
The inhabited subset of a singleton. (Contributed by Jim Kingdon,
10Aug2018.)



Theorem  eqsnm 3714* 
Two ways to express that an inhabited set equals a singleton.
(Contributed by Jim Kingdon, 11Aug2018.)



Theorem  ssprr 3715 
The subsets of a pair. (Contributed by Jim Kingdon, 11Aug2018.)



Theorem  sstpr 3716 
The subsets of a triple. (Contributed by Jim Kingdon, 11Aug2018.)



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



Theorem  tpssi 3718 
A triple of elements of a class is a subset of the class. (Contributed by
Alexander van der Vekens, 1Feb2018.)



Theorem  sneqr 3719 
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 3720 
If a singleton is a subset of another, their members are equal.
(Contributed by NM, 28May2006.)



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



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



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



Theorem  prsspw 3724 
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  preqr1g 3725 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. Closed form of
preqr1 3727. (Contributed by Jim Kingdon, 21Sep2018.)



Theorem  preqr2g 3726 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the second elements are equal. Closed form of
preqr2 3728. (Contributed by Jim Kingdon, 21Sep2018.)



Theorem  preqr1 3727 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same second element, the first elements are equal. (Contributed by
NM, 18Oct1995.)



Theorem  preqr2 3728 
Reverse equality lemma for unordered pairs. If two unordered pairs have
the same first element, the second elements are equal. (Contributed by
NM, 5Aug1993.)



Theorem  preq12b 3729 
Equality relationship for two unordered pairs. (Contributed by NM,
17Oct1996.)



Theorem  prel12 3730 
Equality of two unordered pairs. (Contributed by NM, 17Oct1996.)



Theorem  opthpr 3731 
A way to represent ordered pairs using unordered pairs with distinct
members. (Contributed by NM, 27Mar2007.)



Theorem  preq12bg 3732 
Closed form of preq12b 3729. (Contributed by Scott Fenton,
28Mar2014.)



Theorem  prneimg 3733 
Two pairs are not equal if at least one element of the first pair is not
contained in the second pair. (Contributed by Alexander van der Vekens,
13Aug2017.)



Theorem  preqsn 3734 
Equivalence for a pair equal to a singleton. (Contributed by NM,
3Jun2008.)



Theorem  dfopg 3735 
Value of the ordered pair when the arguments are sets. (Contributed by
Mario Carneiro, 26Apr2015.)



Theorem  dfop 3736 
Value of an ordered pair when the arguments are sets, with the
conclusion corresponding to Kuratowski's original definition.
(Contributed by NM, 25Jun1998.)



Theorem  opeq1 3737 
Equality theorem for ordered pairs. (Contributed by NM, 25Jun1998.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  opeq2 3738 
Equality theorem for ordered pairs. (Contributed by NM, 25Jun1998.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  opeq12 3739 
Equality theorem for ordered pairs. (Contributed by NM, 28May1995.)



Theorem  opeq1i 3740 
Equality inference for ordered pairs. (Contributed by NM,
16Dec2006.)



Theorem  opeq2i 3741 
Equality inference for ordered pairs. (Contributed by NM,
16Dec2006.)



Theorem  opeq12i 3742 
Equality inference for ordered pairs. (Contributed by NM,
16Dec2006.) (Proof shortened by Eric Schmidt, 4Apr2007.)



Theorem  opeq1d 3743 
Equality deduction for ordered pairs. (Contributed by NM,
16Dec2006.)



Theorem  opeq2d 3744 
Equality deduction for ordered pairs. (Contributed by NM,
16Dec2006.)



Theorem  opeq12d 3745 
Equality deduction for ordered pairs. (Contributed by NM, 16Dec2006.)
(Proof shortened by Andrew Salmon, 29Jun2011.)



Theorem  oteq1 3746 
Equality theorem for ordered triples. (Contributed by NM, 3Apr2015.)



Theorem  oteq2 3747 
Equality theorem for ordered triples. (Contributed by NM, 3Apr2015.)



Theorem  oteq3 3748 
Equality theorem for ordered triples. (Contributed by NM, 3Apr2015.)



Theorem  oteq1d 3749 
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11Jan2017.)



Theorem  oteq2d 3750 
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11Jan2017.)



Theorem  oteq3d 3751 
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11Jan2017.)



Theorem  oteq123d 3752 
Equality deduction for ordered triples. (Contributed by Mario Carneiro,
11Jan2017.)



Theorem  nfop 3753 
Boundvariable hypothesis builder for ordered pairs. (Contributed by
NM, 14Nov1995.)



Theorem  nfopd 3754 
Deduction version of boundvariable hypothesis builder nfop 3753.
This
shows how the deduction version of a notfree theorem such as nfop 3753
can
be created from the corresponding notfree inference theorem.
(Contributed by NM, 4Feb2008.)



Theorem  opid 3755 
The ordered pair in Kuratowski's representation.
(Contributed by FL, 28Dec2011.)



Theorem  ralunsn 3756* 
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 3757* 
Double restricted quantification over the union of a set and a
singleton, using implicit substitution. (Contributed by Paul Chapman,
17Nov2012.)



Theorem  opprc 3758 
Expansion of an ordered pair when either member is a proper class.
(Contributed by Mario Carneiro, 26Apr2015.)



Theorem  opprc1 3759 
Expansion of an ordered pair when the first member is a proper class. See
also opprc 3758. (Contributed by NM, 10Apr2004.) (Revised
by Mario
Carneiro, 26Apr2015.)



Theorem  opprc2 3760 
Expansion of an ordered pair when the second member is a proper class.
See also opprc 3758. (Contributed by NM, 15Nov1994.) (Revised
by Mario
Carneiro, 26Apr2015.)



Theorem  oprcl 3761 
If an ordered pair has an element, then its arguments are sets.
(Contributed by Mario Carneiro, 26Apr2015.)



Theorem  pwsnss 3762 
The power set of a singleton. (Contributed by Jim Kingdon,
12Aug2018.)



Theorem  pwpw0ss 3763 
Compute the power set of the power set of the empty set. (See pw0 3699
for
the power set of the empty set.) Theorem 90 of [Suppes] p. 48 (but with
subset in place of equality). (Contributed by Jim Kingdon,
12Aug2018.)



Theorem  pwprss 3764 
The power set of an unordered pair. (Contributed by Jim Kingdon,
13Aug2018.)



Theorem  pwtpss 3765 
The power set of an unordered triple. (Contributed by Jim Kingdon,
13Aug2018.)



Theorem  pwpwpw0ss 3766 
Compute the power set of the power set of the power set of the empty set.
(See also pw0 3699 and pwpw0ss 3763.) (Contributed by Jim Kingdon,
13Aug2018.)



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



2.1.18 The union of a class


Syntax  cuni 3768 
Extend class notation to include the union of a class. Read: "union (of)
".



Definition  dfuni 3769* 
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, . This is
similar to the union of two classes dfun 3102. (Contributed by NM,
23Aug1993.)



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



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



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



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



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



Theorem  nfunid 3775 
Deduction version of nfuni 3774. (Contributed by NM, 18Feb2013.)



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



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



Theorem  unieqi 3778 
Inference of equality of two class unions. (Contributed by NM,
30Aug1993.)



Theorem  unieqd 3779 
Deduction of equality of two class unions. (Contributed by NM,
21Apr1995.)



Theorem  eluniab 3780* 
Membership in union of a class abstraction. (Contributed by NM,
11Aug1994.) (Revised by Mario Carneiro, 14Nov2016.)



Theorem  elunirab 3781* 
Membership in union of a class abstraction. (Contributed by NM,
4Oct2006.)



Theorem  unipr 3782 
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 23Aug1993.)



Theorem  uniprg 3783 
The union of a pair is the union of its members. Proposition 5.7 of
[TakeutiZaring] p. 16.
(Contributed by NM, 25Aug2006.)



Theorem  unisn 3784 
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 30Aug1993.)



Theorem  unisng 3785 
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 13Aug2002.)



Theorem  dfnfc2 3786* 
An alternate statement of the effective freeness of a class , when
it is a set. (Contributed by Mario Carneiro, 14Oct2016.)



Theorem  uniun 3787 
The class union of the union of two classes. Theorem 8.3 of [Quine]
p. 53. (Contributed by NM, 20Aug1993.)



Theorem  uniin 3788 
The class union of the intersection of two classes. Exercise 4.12(n) of
[Mendelson] p. 235. (Contributed by
NM, 4Dec2003.) (Proof shortened
by Andrew Salmon, 29Jun2011.)



Theorem  uniss 3789 
Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
(Contributed by NM, 22Mar1998.) (Proof shortened by Andrew Salmon,
29Jun2011.)



Theorem  ssuni 3790 
Subclass relationship for class union. (Contributed by NM,
24May1994.) (Proof shortened by Andrew Salmon, 29Jun2011.)



Theorem  unissi 3791 
Subclass relationship for subclass union. Inference form of uniss 3789.
(Contributed by David Moews, 1May2017.)



Theorem  unissd 3792 
Subclass relationship for subclass union. Deduction form of uniss 3789.
(Contributed by David Moews, 1May2017.)



Theorem  uni0b 3793 
The union of a set is empty iff the set is included in the singleton of
the empty set. (Contributed by NM, 12Sep2004.)



Theorem  uni0c 3794* 
The union of a set is empty iff all of its members are empty.
(Contributed by NM, 16Aug2006.)



Theorem  uni0 3795 
The union of the empty set is the empty set. Theorem 8.7 of [Quine]
p. 54. (Reproved without relying on axnul by Eric Schmidt.)
(Contributed by NM, 16Sep1993.) (Revised by Eric Schmidt,
4Apr2007.)



Theorem  elssuni 3796 
An element of a class is a subclass of its union. Theorem 8.6 of [Quine]
p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40.
(Contributed by NM, 6Jun1994.)



Theorem  unissel 3797 
Condition turning a subclass relationship for union into an equality.
(Contributed by NM, 18Jul2006.)



Theorem  unissb 3798* 
Relationship involving membership, subset, and union. Exercise 5 of
[Enderton] p. 26 and its converse.
(Contributed by NM, 20Sep2003.)



Theorem  uniss2 3799* 
A subclass condition on the members of two classes that implies a
subclass relation on their unions. Proposition 8.6 of [TakeutiZaring]
p. 59. (Contributed by NM, 22Mar2004.)



Theorem  unidif 3800* 
If the difference
contains the largest
members of , then
the union of the difference is the union of . (Contributed by NM,
22Mar2004.)

