Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



2.1.20 Indexed union and
intersection


Syntax  ciun 3813 
Extend class notation to include indexed union. Note: Historically
(prior to 21Oct2005), set.mm used the notation
, with
the same union symbol as cuni 3736. 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 3814 
Extend class notation to include indexed intersection. Note:
Historically (prior to 21Oct2005), set.mm used the notation
, with the
same intersection symbol as cint 3771. 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 3815* 
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 disjoint variable group (meaning cannot depend on ) and
that and do not share a disjoint
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 3847. Theorem uniiun 3866 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27Jun1998.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dfiun2g 3845* 
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 3846* 
Alternate definition of indexed intersection when is a set.
(Contributed by Jeff Hankins, 27Aug2009.)



Theorem  dfiun2 3847* 
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 3848* 
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 3849* 
Define double indexed union. (Contributed by FL, 6Nov2013.)



Theorem  cbviun 3850* 
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 3851* 
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26Aug2009.) (Revised by Mario Carneiro, 14Oct2016.)



Theorem  cbviunv 3852* 
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 3853* 
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26Aug2009.)



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



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



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



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



Theorem  iunss2 3858* 
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 3767. (Contributed by NM, 9Dec2004.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  iinxsng 3886* 
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 3887* 
Indexed intersection with an unordered pair index. (Contributed by NM,
25Jan2012.)



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



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



Theorem  iunxsngf 3890* 
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25Jun2016.) (Revised by Thierry
Arnoux, 2May2020.)



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



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



Theorem  iunxprg 3893* 
A pair index picks out two instances of an indexed union's argument.
(Contributed by Alexander van der Vekens, 2Feb2018.)



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



Theorem  iinuniss 3895* 
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 3896* 
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 3897 
Subclass relationship for power class and union. (Contributed by NM,
18Jul2006.)



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



Theorem  elpwpw 3899 
Characterization of the elements of a double power class: they are exactly
the sets whose union is included in that class. (Contributed by BJ,
29Apr2021.)



Theorem  pwpwab 3900* 
The double power class written as a class abstraction: the class of sets
whose union is included in the given class. (Contributed by BJ,
29Apr2021.)

