Type  Label  Description 
Statement 

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



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



Theorem  pwpw0ss 3603 
Compute the power set of the power set of the empty set. (See pw0 3539
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 3604 
The power set of an unordered pair. (Contributed by Jim Kingdon,
13Aug2018.)



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



Theorem  pwpwpw0ss 3606 
Compute the power set of the power set of the power set of the empty
set. (See also pw0 3539 and pwpw0ss 3603.) (Contributed by Jim Kingdon,
13Aug2018.)



Theorem  pwv 3607 
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 3608 
Extend class notation to include the union of a class (read: 'union
')



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



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



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



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



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



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



Theorem  nfunid 3615 
Deduction version of nfuni 3614. (Contributed by NM, 18Feb2013.)



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  uniin 3628 
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 3629 
Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.
(Contributed by NM, 22Mar1998.) (Proof shortened by Andrew Salmon,
29Jun2011.)



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



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



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



Theorem  uni0b 3633 
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 3634* 
The union of a set is empty iff all of its members are empty.
(Contributed by NM, 16Aug2006.)



Theorem  uni0 3635 
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 3636 
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 3637 
Condition turning a subclass relationship for union into an equality.
(Contributed by NM, 18Jul2006.)



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



Theorem  uniss2 3639* 
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 3640* 
If the difference
contains the largest
members of , then
the union of the difference is the union of . (Contributed by NM,
22Mar2004.)



Theorem  ssunieq 3641* 
Relationship implying union. (Contributed by NM, 10Nov1999.)



Theorem  unimax 3642* 
Any member of a class is the largest of those members that it includes.
(Contributed by NM, 13Aug2002.)



2.1.19 The intersection of a class


Syntax  cint 3643 
Extend class notation to include the intersection of a class (read:
'intersect ').



Definition  dfint 3644* 
Define the intersection of a class. Definition 7.35 of [TakeutiZaring]
p. 44. For example, { { 1 , 3 } , { 1 , 8 } } = { 1 } .
Compare this with the intersection of two classes, dfin 2952.
(Contributed by NM, 18Aug1993.)



Theorem  dfint2 3645* 
Alternate definition of class intersection. (Contributed by NM,
28Jun1998.)



Theorem  inteq 3646 
Equality law for intersection. (Contributed by NM, 13Sep1999.)



Theorem  inteqi 3647 
Equality inference for class intersection. (Contributed by NM,
2Sep2003.)



Theorem  inteqd 3648 
Equality deduction for class intersection. (Contributed by NM,
2Sep2003.)



Theorem  elint 3649* 
Membership in class intersection. (Contributed by NM, 21May1994.)



Theorem  elint2 3650* 
Membership in class intersection. (Contributed by NM, 14Oct1999.)



Theorem  elintg 3651* 
Membership in class intersection, with the sethood requirement expressed
as an antecedent. (Contributed by NM, 20Nov2003.)



Theorem  elinti 3652 
Membership in class intersection. (Contributed by NM, 14Oct1999.)
(Proof shortened by Andrew Salmon, 9Jul2011.)



Theorem  nfint 3653 
Boundvariable hypothesis builder for intersection. (Contributed by NM,
2Feb1997.) (Proof shortened by Andrew Salmon, 12Aug2011.)



Theorem  elintab 3654* 
Membership in the intersection of a class abstraction. (Contributed by
NM, 30Aug1993.)



Theorem  elintrab 3655* 
Membership in the intersection of a class abstraction. (Contributed by
NM, 17Oct1999.)



Theorem  elintrabg 3656* 
Membership in the intersection of a class abstraction. (Contributed by
NM, 17Feb2007.)



Theorem  int0 3657 
The intersection of the empty set is the universal class. Exercise 2 of
[TakeutiZaring] p. 44.
(Contributed by NM, 18Aug1993.)



Theorem  intss1 3658 
An element of a class includes the intersection of the class. Exercise
4 of [TakeutiZaring] p. 44 (with
correction), generalized to classes.
(Contributed by NM, 18Nov1995.)



Theorem  ssint 3659* 
Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52
and its converse. (Contributed by NM, 14Oct1999.)



Theorem  ssintab 3660* 
Subclass of the intersection of a class abstraction. (Contributed by
NM, 31Jul2006.) (Proof shortened by Andrew Salmon, 9Jul2011.)



Theorem  ssintub 3661* 
Subclass of the least upper bound. (Contributed by NM, 8Aug2000.)



Theorem  ssmin 3662* 
Subclass of the minimum value of class of supersets. (Contributed by
NM, 10Aug2006.)



Theorem  intmin 3663* 
Any member of a class is the smallest of those members that include it.
(Contributed by NM, 13Aug2002.) (Proof shortened by Andrew Salmon,
9Jul2011.)



Theorem  intss 3664 
Intersection of subclasses. (Contributed by NM, 14Oct1999.)



Theorem  intssunim 3665* 
The intersection of an inhabited set is a subclass of its union.
(Contributed by NM, 29Jul2006.)



Theorem  ssintrab 3666* 
Subclass of the intersection of a restricted class builder.
(Contributed by NM, 30Jan2015.)



Theorem  intssuni2m 3667* 
Subclass relationship for intersection and union. (Contributed by Jim
Kingdon, 14Aug2018.)



Theorem  intminss 3668* 
Under subset ordering, the intersection of a restricted class
abstraction is less than or equal to any of its members. (Contributed
by NM, 7Sep2013.)



Theorem  intmin2 3669* 
Any set is the smallest of all sets that include it. (Contributed by
NM, 20Sep2003.)



Theorem  intmin3 3670* 
Under subset ordering, the intersection of a class abstraction is less
than or equal to any of its members. (Contributed by NM,
3Jul2005.)



Theorem  intmin4 3671* 
Elimination of a conjunct in a class intersection. (Contributed by NM,
31Jul2006.)



Theorem  intab 3672* 
The intersection of a special case of a class abstraction. may be
free in
and , which can be
thought of a and
. (Contributed by NM, 28Jul2006.) (Proof shortened by
Mario Carneiro, 14Nov2016.)



Theorem  int0el 3673 
The intersection of a class containing the empty set is empty.
(Contributed by NM, 24Apr2004.)



Theorem  intun 3674 
The class intersection of the union of two classes. Theorem 78 of
[Suppes] p. 42. (Contributed by NM,
22Sep2002.)



Theorem  intpr 3675 
The intersection of a pair is the intersection of its members. Theorem
71 of [Suppes] p. 42. (Contributed by
NM, 14Oct1999.)



Theorem  intprg 3676 
The intersection of a pair is the intersection of its members. Closed
form of intpr 3675. Theorem 71 of [Suppes] p. 42. (Contributed by FL,
27Apr2008.)



Theorem  intsng 3677 
Intersection of a singleton. (Contributed by Stefan O'Rear,
22Feb2015.)



Theorem  intsn 3678 
The intersection of a singleton is its member. Theorem 70 of [Suppes]
p. 41. (Contributed by NM, 29Sep2002.)



Theorem  uniintsnr 3679* 
The union and intersection of a singleton are equal. See also eusn 3472.
(Contributed by Jim Kingdon, 14Aug2018.)



Theorem  uniintabim 3680 
The union and the intersection of a class abstraction are equal if there
is a unique satisfying value of . (Contributed by Jim
Kingdon, 14Aug2018.)



Theorem  intunsn 3681 
Theorem joining a singleton to an intersection. (Contributed by NM,
29Sep2002.)



Theorem  rint0 3682 
Relative intersection of an empty set. (Contributed by Stefan O'Rear,
3Apr2015.)



Theorem  elrint 3683* 
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3Apr2015.)



Theorem  elrint2 3684* 
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3Apr2015.)



2.1.20 Indexed union and
intersection


Syntax  ciun 3685 
Extend class notation to include indexed union. Note: Historically
(prior to 21Oct2005), set.mm used the notation
, with
the same union symbol as cuni 3608. While that syntax was unambiguous, it
did not allow for LALR parsing of the syntax constructions in set.mm. The
new syntax uses as distinguished symbol instead of and does
allow LALR parsing. Thanks to Peter Backes for suggesting this change.



Syntax  ciin 3686 
Extend class notation to include indexed intersection. Note:
Historically (prior to 21Oct2005), set.mm used the notation
, with the
same intersection symbol as cint 3643. Although
that syntax was unambiguous, it did not allow for LALR parsing of the
syntax constructions in set.mm. The new syntax uses a distinguished
symbol
instead of and
does allow LALR parsing. Thanks to
Peter Backes for suggesting this change.



Definition  dfiun 3687* 
Define indexed union. Definition indexed union in [Stoll] p. 45. In
most applications, is independent of (although this is not
required by the definition), and depends on i.e. can be read
informally as . We call the index, the index
set, and the
indexed set. In most books, is written as
a subscript or underneath a union symbol . We use a special
union symbol to make it easier to distinguish from plain class
union. In many theorems, you will see that and are in the
same distinct variable group (meaning cannot depend on ) and
that and do not share a distinct
variable group (meaning
that can be thought of as i.e. can be substituted with a
class expression containing ). An alternate definition tying
indexed union to ordinary union is dfiun2 3719. Theorem uniiun 3738 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27Jun1998.)



Definition  dfiin 3688* 
Define indexed intersection. Definition of [Stoll] p. 45. See the
remarks for its sibling operation of indexed union dfiun 3687. An
alternate definition tying indexed intersection to ordinary intersection
is dfiin2 3720. Theorem intiin 3739 provides a definition of ordinary
intersection in terms of indexed intersection. (Contributed by NM,
27Jun1998.)



Theorem  eliun 3689* 
Membership in indexed union. (Contributed by NM, 3Sep2003.)



Theorem  eliin 3690* 
Membership in indexed intersection. (Contributed by NM, 3Sep2003.)



Theorem  iuncom 3691* 
Commutation of indexed unions. (Contributed by NM, 18Dec2008.)



Theorem  iuncom4 3692 
Commutation of union with indexed union. (Contributed by Mario
Carneiro, 18Jan2014.)



Theorem  iunconstm 3693* 
Indexed union of a constant class, i.e. where does not depend on
. (Contributed
by Jim Kingdon, 15Aug2018.)



Theorem  iinconstm 3694* 
Indexed intersection of a constant class, i.e. where does not
depend on .
(Contributed by Jim Kingdon, 19Dec2018.)



Theorem  iuniin 3695* 
Law combining indexed union with indexed intersection. Eq. 14 in
[KuratowskiMostowski] p.
109. This theorem also appears as the last
example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29.
(Contributed by NM, 17Aug2004.) (Proof shortened by Andrew Salmon,
25Jul2011.)



Theorem  iunss1 3696* 
Subclass theorem for indexed union. (Contributed by NM, 10Dec2004.)
(Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  iinss1 3697* 
Subclass theorem for indexed union. (Contributed by NM,
24Jan2012.)



Theorem  iuneq1 3698* 
Equality theorem for indexed union. (Contributed by NM,
27Jun1998.)



Theorem  iineq1 3699* 
Equality theorem for restricted existential quantifier. (Contributed by
NM, 27Jun1998.)



Theorem  ss2iun 3700 
Subclass theorem for indexed union. (Contributed by NM, 26Nov2003.)
(Proof shortened by Andrew Salmon, 25Jul2011.)

