Type  Label  Description 
Statement 

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



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



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



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



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



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



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



Theorem  uniintabim 3708 
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 3709 
Theorem joining a singleton to an intersection. (Contributed by NM,
29Sep2002.)



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



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



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



2.1.20 Indexed union and
intersection


Syntax  ciun 3713 
Extend class notation to include indexed union. Note: Historically
(prior to 21Oct2005), set.mm used the notation
, with
the same union symbol as cuni 3636. 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 3714 
Extend class notation to include indexed intersection. Note:
Historically (prior to 21Oct2005), set.mm used the notation
, with the
same intersection symbol as cint 3671. 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 3715* 
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 3747. Theorem uniiun 3766 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27Jun1998.)



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



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



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



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



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



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



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



Theorem  iuniin 3723* 
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 3724* 
Subclass theorem for indexed union. (Contributed by NM, 10Dec2004.)
(Proof shortened by Andrew Salmon, 25Jul2011.)



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



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



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



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



Theorem  iuneq2 3729 
Equality theorem for indexed union. (Contributed by NM,
22Oct2003.)



Theorem  iineq2 3730 
Equality theorem for indexed intersection. (Contributed by NM,
22Oct2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  iuneq2i 3731 
Equality inference for indexed union. (Contributed by NM,
22Oct2003.)



Theorem  iineq2i 3732 
Equality inference for indexed intersection. (Contributed by NM,
22Oct2003.)



Theorem  iineq2d 3733 
Equality deduction for indexed intersection. (Contributed by NM,
7Dec2011.)



Theorem  iuneq2dv 3734* 
Equality deduction for indexed union. (Contributed by NM,
3Aug2004.)



Theorem  iineq2dv 3735* 
Equality deduction for indexed intersection. (Contributed by NM,
3Aug2004.)



Theorem  iuneq1d 3736* 
Equality theorem for indexed union, deduction version. (Contributed by
Drahflow, 22Oct2015.)



Theorem  iuneq12d 3737* 
Equality deduction for indexed union, deduction version. (Contributed
by Drahflow, 22Oct2015.)



Theorem  iuneq2d 3738* 
Equality deduction for indexed union. (Contributed by Drahflow,
22Oct2015.)



Theorem  nfiunxy 3739* 
Boundvariable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25Jan2014.)



Theorem  nfiinxy 3740* 
Boundvariable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25Jan2014.)



Theorem  nfiunya 3741* 
Boundvariable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25Jan2014.)



Theorem  nfiinya 3742* 
Boundvariable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25Jan2014.)



Theorem  nfiu1 3743 
Boundvariable hypothesis builder for indexed union. (Contributed by
NM, 12Oct2003.)



Theorem  nfii1 3744 
Boundvariable hypothesis builder for indexed intersection.
(Contributed by NM, 15Oct2003.)



Theorem  dfiun2g 3745* 
Alternate definition of indexed union when is a set. Definition
15(a) of [Suppes] p. 44. (Contributed by
NM, 23Mar2006.) (Proof
shortened by Andrew Salmon, 25Jul2011.)



Theorem  dfiin2g 3746* 
Alternate definition of indexed intersection when is a set.
(Contributed by Jeff Hankins, 27Aug2009.)



Theorem  dfiun2 3747* 
Alternate definition of indexed union when is a set. Definition
15(a) of [Suppes] p. 44. (Contributed by
NM, 27Jun1998.) (Revised by
David Abernethy, 19Jun2012.)



Theorem  dfiin2 3748* 
Alternate definition of indexed intersection when is a set.
Definition 15(b) of [Suppes] p. 44.
(Contributed by NM, 28Jun1998.)
(Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  dfiunv2 3749* 
Define double indexed union. (Contributed by FL, 6Nov2013.)



Theorem  cbviun 3750* 
Rule used to change the bound variables in an indexed union, with the
substitution specified implicitly by the hypothesis. (Contributed by
NM, 26Mar2006.) (Revised by Andrew Salmon, 25Jul2011.)



Theorem  cbviin 3751* 
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26Aug2009.) (Revised by Mario Carneiro, 14Oct2016.)



Theorem  cbviunv 3752* 
Rule used to change the bound variables in an indexed union, with the
substitution specified implicitly by the hypothesis. (Contributed by
NM, 15Sep2003.)



Theorem  cbviinv 3753* 
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26Aug2009.)



Theorem  iunss 3754* 
Subset theorem for an indexed union. (Contributed by NM, 13Sep2003.)
(Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  ssiun 3755* 
Subset implication for an indexed union. (Contributed by NM,
3Sep2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  ssiun2 3756 
Identity law for subset of an indexed union. (Contributed by NM,
12Oct2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  ssiun2s 3757* 
Subset relationship for an indexed union. (Contributed by NM,
26Oct2003.)



Theorem  iunss2 3758* 
A subclass condition on the members of two indexed classes
and that implies a subclass relation on their indexed
unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59.
Compare uniss2 3667. (Contributed by NM, 9Dec2004.)



Theorem  iunab 3759* 
The indexed union of a class abstraction. (Contributed by NM,
27Dec2004.)



Theorem  iunrab 3760* 
The indexed union of a restricted class abstraction. (Contributed by
NM, 3Jan2004.) (Proof shortened by Mario Carneiro, 14Nov2016.)



Theorem  iunxdif2 3761* 
Indexed union with a class difference as its index. (Contributed by NM,
10Dec2004.)



Theorem  ssiinf 3762 
Subset theorem for an indexed intersection. (Contributed by FL,
15Oct2012.) (Proof shortened by Mario Carneiro, 14Oct2016.)



Theorem  ssiin 3763* 
Subset theorem for an indexed intersection. (Contributed by NM,
15Oct2003.)



Theorem  iinss 3764* 
Subset implication for an indexed intersection. (Contributed by NM,
15Oct2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  iinss2 3765 
An indexed intersection is included in any of its members. (Contributed
by FL, 15Oct2012.)



Theorem  uniiun 3766* 
Class union in terms of indexed union. Definition in [Stoll] p. 43.
(Contributed by NM, 28Jun1998.)



Theorem  intiin 3767* 
Class intersection in terms of indexed intersection. Definition in
[Stoll] p. 44. (Contributed by NM,
28Jun1998.)



Theorem  iunid 3768* 
An indexed union of singletons recovers the index set. (Contributed by
NM, 6Sep2005.)



Theorem  iun0 3769 
An indexed union of the empty set is empty. (Contributed by NM,
26Mar2003.) (Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  0iun 3770 
An empty indexed union is empty. (Contributed by NM, 4Dec2004.)
(Proof shortened by Andrew Salmon, 25Jul2011.)



Theorem  0iin 3771 
An empty indexed intersection is the universal class. (Contributed by
NM, 20Oct2005.)



Theorem  viin 3772* 
Indexed intersection with a universal index class. (Contributed by NM,
11Sep2008.)



Theorem  iunn0m 3773* 
There is an inhabited class in an indexed collection iff the
indexed union of them is inhabited. (Contributed by Jim Kingdon,
16Aug2018.)



Theorem  iinab 3774* 
Indexed intersection of a class builder. (Contributed by NM,
6Dec2011.)



Theorem  iinrabm 3775* 
Indexed intersection of a restricted class builder. (Contributed by Jim
Kingdon, 16Aug2018.)



Theorem  iunin2 3776* 
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3766 to recover
Enderton's theorem. (Contributed by NM, 26Mar2004.)



Theorem  iunin1 3777* 
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3766 to recover
Enderton's theorem. (Contributed by Mario Carneiro, 30Aug2015.)



Theorem  iundif2ss 3778* 
Indexed union of class difference. Compare to theorem "De Morgan's
laws" in [Enderton] p. 31.
(Contributed by Jim Kingdon,
17Aug2018.)



Theorem  2iunin 3779* 
Rearrange indexed unions over intersection. (Contributed by NM,
18Dec2008.)



Theorem  iindif2m 3780* 
Indexed intersection of class difference. Compare to Theorem "De
Morgan's laws" in [Enderton] p.
31. (Contributed by Jim Kingdon,
17Aug2018.)



Theorem  iinin2m 3781* 
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17Aug2018.)



Theorem  iinin1m 3782* 
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17Aug2018.)



Theorem  elriin 3783* 
Elementhood in a relative intersection. (Contributed by Mario Carneiro,
30Dec2016.)



Theorem  riin0 3784* 
Relative intersection of an empty family. (Contributed by Stefan
O'Rear, 3Apr2015.)



Theorem  riinm 3785* 
Relative intersection of an inhabited family. (Contributed by Jim
Kingdon, 19Aug2018.)



Theorem  iinxsng 3786* 
A singleton index picks out an instance of an indexed intersection's
argument. (Contributed by NM, 15Jan2012.) (Proof shortened by Mario
Carneiro, 17Nov2016.)



Theorem  iinxprg 3787* 
Indexed intersection with an unordered pair index. (Contributed by NM,
25Jan2012.)



Theorem  iunxsng 3788* 
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25Jun2016.)



Theorem  iunxsn 3789* 
A singleton index picks out an instance of an indexed union's argument.
(Contributed by NM, 26Mar2004.) (Proof shortened by Mario Carneiro,
25Jun2016.)



Theorem  iunun 3790 
Separate a union in an indexed union. (Contributed by NM, 27Dec2004.)
(Proof shortened by Mario Carneiro, 17Nov2016.)



Theorem  iunxun 3791 
Separate a union in the index of an indexed union. (Contributed by NM,
26Mar2004.) (Proof shortened by Mario Carneiro, 17Nov2016.)



Theorem  iunxiun 3792* 
Separate an indexed union in the index of an indexed union.
(Contributed by Mario Carneiro, 5Dec2016.)



Theorem  iinuniss 3793* 
A relationship involving union and indexed intersection. Exercise 23 of
[Enderton] p. 33 but with equality
changed to subset. (Contributed by
Jim Kingdon, 19Aug2018.)



Theorem  iununir 3794* 
A relationship involving union and indexed union. Exercise 25 of
[Enderton] p. 33 but with biconditional
changed to implication.
(Contributed by Jim Kingdon, 19Aug2018.)



Theorem  sspwuni 3795 
Subclass relationship for power class and union. (Contributed by NM,
18Jul2006.)



Theorem  pwssb 3796* 
Two ways to express a collection of subclasses. (Contributed by NM,
19Jul2006.)



Theorem  elpwuni 3797 
Relationship for power class and union. (Contributed by NM,
18Jul2006.)



Theorem  iinpw 3798* 
The power class of an intersection in terms of indexed intersection.
Exercise 24(a) of [Enderton] p. 33.
(Contributed by NM,
29Nov2003.)



Theorem  iunpwss 3799* 
Inclusion of an indexed union of a power class in the power class of the
union of its index. Part of Exercise 24(b) of [Enderton] p. 33.
(Contributed by NM, 25Nov2003.)



Theorem  rintm 3800* 
Relative intersection of an inhabited class. (Contributed by Jim
Kingdon, 19Aug2018.)

