Theorem List for Intuitionistic Logic Explorer - 3801-3900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | intssunim 3801* |
The intersection of an inhabited set is a subclass of its union.
(Contributed by NM, 29-Jul-2006.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![|^| |^|](bigcap.gif) ![U.
U.](bigcup.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ssintrab 3802* |
Subclass of the intersection of a restricted class builder.
(Contributed by NM, 30-Jan-2015.)
|
![( (](lp.gif) ![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | intssuni2m 3803* |
Subclass relationship for intersection and union. (Contributed by Jim
Kingdon, 14-Aug-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A A](_ca.gif) ![|^| |^|](bigcap.gif)
![U. U.](bigcup.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | intminss 3804* |
Under subset ordering, the intersection of a restricted class
abstraction is less than or equal to any of its members. (Contributed
by NM, 7-Sep-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | intmin2 3805* |
Any set is the smallest of all sets that include it. (Contributed by
NM, 20-Sep-2003.)
|
![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![A A](_ca.gif) |
|
Theorem | intmin3 3806* |
Under subset ordering, the intersection of a class abstraction is less
than or equal to any of its members. (Contributed by NM,
3-Jul-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif)
![|^| |^|](bigcap.gif) ![{
{](lbrace.gif) ![ph ph](_varphi.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | intmin4 3807* |
Elimination of a conjunct in a class intersection. (Contributed by NM,
31-Jul-2006.)
|
![( (](lp.gif) ![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![|^| |^|](bigcap.gif) ![{
{](lbrace.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | intab 3808* |
The intersection of a special case of a class abstraction. may be
free in
and , which can be
thought of a ![ph ph](_varphi.gif) ![( (](lp.gif) ![y y](_y.gif) and
![A A](_ca.gif) ![( (](lp.gif) ![y y](_y.gif) . (Contributed by NM, 28-Jul-2006.) (Proof shortened by
Mario Carneiro, 14-Nov-2016.)
|
![{ {](lbrace.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | int0el 3809 |
The intersection of a class containing the empty set is empty.
(Contributed by NM, 24-Apr-2004.)
|
![( (](lp.gif)
![|^|
|^|](bigcap.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | intun 3810 |
The class intersection of the union of two classes. Theorem 78 of
[Suppes] p. 42. (Contributed by NM,
22-Sep-2002.)
|
![|^|
|^|](bigcap.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![|^| |^|](bigcap.gif) ![|^| |^|](bigcap.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | intpr 3811 |
The intersection of a pair is the intersection of its members. Theorem
71 of [Suppes] p. 42. (Contributed by
NM, 14-Oct-1999.)
|
![|^|
|^|](bigcap.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | intprg 3812 |
The intersection of a pair is the intersection of its members. Closed
form of intpr 3811. Theorem 71 of [Suppes] p. 42. (Contributed by FL,
27-Apr-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | intsng 3813 |
Intersection of a singleton. (Contributed by Stefan O'Rear,
22-Feb-2015.)
|
![( (](lp.gif) ![|^|
|^|](bigcap.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | intsn 3814 |
The intersection of a singleton is its member. Theorem 70 of [Suppes]
p. 41. (Contributed by NM, 29-Sep-2002.)
|
![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![A A](_ca.gif) |
|
Theorem | uniintsnr 3815* |
The union and intersection of a singleton are equal. See also eusn 3605.
(Contributed by Jim Kingdon, 14-Aug-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![U. U.](bigcup.gif) ![|^| |^|](bigcap.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | uniintabim 3816 |
The union and the intersection of a class abstraction are equal if there
is a unique satisfying value of ![ph ph](_varphi.gif) ![( (](lp.gif) ![x x](_x.gif) . (Contributed by Jim
Kingdon, 14-Aug-2018.)
|
![( (](lp.gif) ![E! E!](_e1.gif) ![x x](_x.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | intunsn 3817 |
Theorem joining a singleton to an intersection. (Contributed by NM,
29-Sep-2002.)
|
![|^| |^|](bigcap.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![|^| |^|](bigcap.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | rint0 3818 |
Relative intersection of an empty set. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif)
![|^| |^|](bigcap.gif) ![X X](_cx.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | elrint 3819* |
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![|^| |^|](bigcap.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | elrint2 3820* |
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|^| |^|](bigcap.gif) ![B B](_cb.gif) ![A. A.](forall.gif)
![y y](_y.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
2.1.20 Indexed union and
intersection
|
|
Syntax | ciun 3821 |
Extend class notation to include indexed union. Note: Historically
(prior to 21-Oct-2005), set.mm used the notation ![U. U.](bigcup.gif)
![A A](_ca.gif) , with
the same union symbol as cuni 3744. 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.
|
![U_ U_](_cupbar.gif) ![B B](_cb.gif) |
|
Syntax | ciin 3822 |
Extend class notation to include indexed intersection. Note:
Historically (prior to 21-Oct-2005), set.mm used the notation
![|^| |^|](bigcap.gif) ![A A](_ca.gif) , with the
same intersection symbol as cint 3779. 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.
|
![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif) |
|
Definition | df-iun 3823* |
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 ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) . 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 ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) i.e. can be substituted with a
class expression containing ). An alternate definition tying
indexed union to ordinary union is dfiun2 3855. Theorem uniiun 3874 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27-Jun-1998.)
|
![U_ U_](_cupbar.gif)
![{ {](lbrace.gif) ![E. E.](exists.gif)
![B B](_cb.gif) ![} }](rbrace.gif) |
|
Definition | df-iin 3824* |
Define indexed intersection. Definition of [Stoll] p. 45. See the
remarks for its sibling operation of indexed union df-iun 3823. An
alternate definition tying indexed intersection to ordinary intersection
is dfiin2 3856. Theorem intiin 3875 provides a definition of ordinary
intersection in terms of indexed intersection. (Contributed by NM,
27-Jun-1998.)
|
![|^|_ |^|_](_capbar.gif) ![{ {](lbrace.gif) ![A. A.](forall.gif)
![B B](_cb.gif) ![} }](rbrace.gif) |
|
Theorem | eliun 3825* |
Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
|
![( (](lp.gif) ![U_ U_](_cupbar.gif)
![E. E.](exists.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | eliin 3826* |
Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
|
![( (](lp.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![A. A.](forall.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | iuncom 3827* |
Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
|
![U_ U_](_cupbar.gif)
![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![C C](_cc.gif) |
|
Theorem | iuncom4 3828 |
Commutation of union with indexed union. (Contributed by Mario
Carneiro, 18-Jan-2014.)
|
![U_ U_](_cupbar.gif)
![U. U.](bigcup.gif) ![U. U.](bigcup.gif) ![U_ U_](_cupbar.gif) ![B B](_cb.gif) |
|
Theorem | iunconstm 3829* |
Indexed union of a constant class, i.e. where does not depend on
. (Contributed
by Jim Kingdon, 15-Aug-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![U_ U_](_cupbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | iinconstm 3830* |
Indexed intersection of a constant class, i.e. where does not
depend on .
(Contributed by Jim Kingdon, 19-Dec-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | iuniin 3831* |
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, 17-Aug-2004.) (Proof shortened by Andrew Salmon,
25-Jul-2011.)
|
![U_ U_](_cupbar.gif)
![|^|_ |^|_](_capbar.gif) ![|^|_ |^|_](_capbar.gif) ![U_ U_](_cupbar.gif)
![C C](_cc.gif) |
|
Theorem | iunss1 3832* |
Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![( (](lp.gif) ![U_
U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iinss1 3833* |
Subclass theorem for indexed union. (Contributed by NM,
24-Jan-2012.)
|
![( (](lp.gif) ![|^|_
|^|_](_capbar.gif)
![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iuneq1 3834* |
Equality theorem for indexed union. (Contributed by NM,
27-Jun-1998.)
|
![( (](lp.gif) ![U_
U_](_cupbar.gif)
![U_ U_](_cupbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iineq1 3835* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 27-Jun-1998.)
|
![( (](lp.gif) ![|^|_
|^|_](_capbar.gif)
![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ss2iun 3836 |
Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![U_
U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iuneq2 3837 |
Equality theorem for indexed union. (Contributed by NM,
22-Oct-2003.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![U_
U_](_cupbar.gif)
![U_ U_](_cupbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iineq2 3838 |
Equality theorem for indexed intersection. (Contributed by NM,
22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![|^|_
|^|_](_capbar.gif)
![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iuneq2i 3839 |
Equality inference for indexed union. (Contributed by NM,
22-Oct-2003.)
|
![( (](lp.gif) ![C C](_cc.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![C C](_cc.gif) |
|
Theorem | iineq2i 3840 |
Equality inference for indexed intersection. (Contributed by NM,
22-Oct-2003.)
|
![( (](lp.gif) ![C C](_cc.gif) ![|^|_ |^|_](_capbar.gif) ![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) |
|
Theorem | iineq2d 3841 |
Equality deduction for indexed intersection. (Contributed by NM,
7-Dec-2011.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif)
![|^|_ |^|_](_capbar.gif) ![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iuneq2dv 3842* |
Equality deduction for indexed union. (Contributed by NM,
3-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iineq2dv 3843* |
Equality deduction for indexed intersection. (Contributed by NM,
3-Aug-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iuneq1d 3844* |
Equality theorem for indexed union, deduction version. (Contributed by
Drahflow, 22-Oct-2015.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iuneq12d 3845* |
Equality deduction for indexed union, deduction version. (Contributed
by Drahflow, 22-Oct-2015.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | iuneq2d 3846* |
Equality deduction for indexed union. (Contributed by Drahflow,
22-Oct-2015.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | nfiunxy 3847* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![U_ U_](_cupbar.gif) ![B B](_cb.gif) |
|
Theorem | nfiinxy 3848* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif) |
|
Theorem | nfiunya 3849* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![U_ U_](_cupbar.gif) ![B B](_cb.gif) |
|
Theorem | nfiinya 3850* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif) |
|
Theorem | nfiu1 3851 |
Bound-variable hypothesis builder for indexed union. (Contributed by
NM, 12-Oct-2003.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![U_ U_](_cupbar.gif) ![B B](_cb.gif) |
|
Theorem | nfii1 3852 |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by NM, 15-Oct-2003.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif) |
|
Theorem | dfiun2g 3853* |
Alternate definition of indexed union when is a set. Definition
15(a) of [Suppes] p. 44. (Contributed by
NM, 23-Mar-2006.) (Proof
shortened by Andrew Salmon, 25-Jul-2011.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![U_
U_](_cupbar.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif)
![B B](_cb.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | dfiin2g 3854* |
Alternate definition of indexed intersection when is a set.
(Contributed by Jeff Hankins, 27-Aug-2009.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![|^|_
|^|_](_capbar.gif)
![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif)
![B B](_cb.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | dfiun2 3855* |
Alternate definition of indexed union when is a set. Definition
15(a) of [Suppes] p. 44. (Contributed by
NM, 27-Jun-1998.) (Revised by
David Abernethy, 19-Jun-2012.)
|
![U_ U_](_cupbar.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif)
![B B](_cb.gif) ![} }](rbrace.gif) |
|
Theorem | dfiin2 3856* |
Alternate definition of indexed intersection when is a set.
Definition 15(b) of [Suppes] p. 44.
(Contributed by NM, 28-Jun-1998.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![|^|_ |^|_](_capbar.gif)
![|^| |^|](bigcap.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif)
![B B](_cb.gif) ![} }](rbrace.gif) |
|
Theorem | dfiunv2 3857* |
Define double indexed union. (Contributed by FL, 6-Nov-2013.)
|
![U_ U_](_cupbar.gif)
![U_ U_](_cupbar.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![C C](_cc.gif) ![} }](rbrace.gif) |
|
Theorem | cbviun 3858* |
Rule used to change the bound variables in an indexed union, with the
substitution specified implicitly by the hypothesis. (Contributed by
NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif)
![C C](_cc.gif) ![U_ U_](_cupbar.gif)
![U_ U_](_cupbar.gif) ![C C](_cc.gif) |
|
Theorem | cbviin 3859* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif)
![C C](_cc.gif) ![|^|_ |^|_](_capbar.gif)
![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) |
|
Theorem | cbviunv 3860* |
Rule used to change the bound variables in an indexed union, with the
substitution specified implicitly by the hypothesis. (Contributed by
NM, 15-Sep-2003.)
|
![( (](lp.gif) ![C C](_cc.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![C C](_cc.gif) |
|
Theorem | cbviinv 3861* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.)
|
![( (](lp.gif) ![C C](_cc.gif) ![|^|_ |^|_](_capbar.gif) ![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) |
|
Theorem | iunss 3862* |
Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![( (](lp.gif) ![U_ U_](_cupbar.gif) ![A. A.](forall.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ssiun 3863* |
Subset implication for an indexed union. (Contributed by NM,
3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![( (](lp.gif) ![E. E.](exists.gif)
![U_ U_](_cupbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ssiun2 3864 |
Identity law for subset of an indexed union. (Contributed by NM,
12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![( (](lp.gif)
![U_ U_](_cupbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ssiun2s 3865* |
Subset relationship for an indexed union. (Contributed by NM,
26-Oct-2003.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![U_ U_](_cupbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | iunss2 3866* |
A subclass condition on the members of two indexed classes ![C C](_cc.gif) ![(
(](lp.gif) ![x x](_x.gif)
and ![D D](_cd.gif) ![( (](lp.gif) ![y y](_y.gif) that implies a subclass relation on their indexed
unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59.
Compare uniss2 3775. (Contributed by NM, 9-Dec-2004.)
|
![( (](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![U_
U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | iunab 3867* |
The indexed union of a class abstraction. (Contributed by NM,
27-Dec-2004.)
|
![U_ U_](_cupbar.gif)
![{ {](lbrace.gif)
![ph ph](_varphi.gif) ![{ {](lbrace.gif)
![E. E.](exists.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) |
|
Theorem | iunrab 3868* |
The indexed union of a restricted class abstraction. (Contributed by
NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|
![U_ U_](_cupbar.gif)
![{ {](lbrace.gif)
![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![}
}](rbrace.gif) |
|
Theorem | iunxdif2 3869* |
Indexed union with a class difference as its index. (Contributed by NM,
10-Dec-2004.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![U_ U_](_cupbar.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![U_ U_](_cupbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ssiinf 3870 |
Subset theorem for an indexed intersection. (Contributed by FL,
15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![A. A.](forall.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ssiin 3871* |
Subset theorem for an indexed intersection. (Contributed by NM,
15-Oct-2003.)
|
![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![A. A.](forall.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | iinss 3872* |
Subset implication for an indexed intersection. (Contributed by NM,
15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![|^|_
|^|_](_capbar.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iinss2 3873 |
An indexed intersection is included in any of its members. (Contributed
by FL, 15-Oct-2012.)
|
![( (](lp.gif) ![|^|_
|^|_](_capbar.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | uniiun 3874* |
Class union in terms of indexed union. Definition in [Stoll] p. 43.
(Contributed by NM, 28-Jun-1998.)
|
![U.
U.](bigcup.gif) ![U_ U_](_cupbar.gif)
![x x](_x.gif) |
|
Theorem | intiin 3875* |
Class intersection in terms of indexed intersection. Definition in
[Stoll] p. 44. (Contributed by NM,
28-Jun-1998.)
|
![|^|
|^|](bigcap.gif)
![|^|_ |^|_](_capbar.gif) ![x x](_x.gif) |
|
Theorem | iunid 3876* |
An indexed union of singletons recovers the index set. (Contributed by
NM, 6-Sep-2005.)
|
![U_ U_](_cupbar.gif)
![{ {](lbrace.gif) ![x x](_x.gif) ![A A](_ca.gif) |
|
Theorem | iun0 3877 |
An indexed union of the empty set is empty. (Contributed by NM,
26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![U_ U_](_cupbar.gif)
![(/) (/)](varnothing.gif) |
|
Theorem | 0iun 3878 |
An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
![U_ U_](_cupbar.gif)
![(/) (/)](varnothing.gif) |
|
Theorem | 0iin 3879 |
An empty indexed intersection is the universal class. (Contributed by
NM, 20-Oct-2005.)
|
![|^|_ |^|_](_capbar.gif) ![_V _V](rmcv.gif) |
|
Theorem | viin 3880* |
Indexed intersection with a universal index class. (Contributed by NM,
11-Sep-2008.)
|
![|^|_ |^|_](_capbar.gif) ![{ {](lbrace.gif) ![A. A.](forall.gif)
![A A](_ca.gif) ![} }](rbrace.gif) |
|
Theorem | iunn0m 3881* |
There is an inhabited class in an indexed collection ![B B](_cb.gif) ![(
(](lp.gif) ![x x](_x.gif) iff the
indexed union of them is inhabited. (Contributed by Jim Kingdon,
16-Aug-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![U_ U_](_cupbar.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | iinab 3882* |
Indexed intersection of a class builder. (Contributed by NM,
6-Dec-2011.)
|
![|^|_ |^|_](_capbar.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif)
![A. A.](forall.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) |
|
Theorem | iinrabm 3883* |
Indexed intersection of a restricted class builder. (Contributed by Jim
Kingdon, 16-Aug-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![|^|_ |^|_](_capbar.gif) ![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif)
![A. A.](forall.gif) ![ph ph](_varphi.gif) ![}
}](rbrace.gif) ![) )](rp.gif) |
|
Theorem | iunin2 3884* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3874 to recover
Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
|
![U_ U_](_cupbar.gif)
![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iunin1 3885* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3874 to recover
Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
|
![U_ U_](_cupbar.gif)
![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | iundif2ss 3886* |
Indexed union of class difference. Compare to theorem "De Morgan's
laws" in [Enderton] p. 31.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
![U_ U_](_cupbar.gif)
![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | 2iunin 3887* |
Rearrange indexed unions over intersection. (Contributed by NM,
18-Dec-2008.)
|
![U_ U_](_cupbar.gif)
![U_ U_](_cupbar.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | iindif2m 3888* |
Indexed intersection of class difference. Compare to Theorem "De
Morgan's laws" in [Enderton] p.
31. (Contributed by Jim Kingdon,
17-Aug-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![|^|_ |^|_](_capbar.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![U_ U_](_cupbar.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iinin2m 3889* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![|^|_ |^|_](_capbar.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iinin1m 3890* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![|^|_ |^|_](_capbar.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elriin 3891* |
Elementhood in a relative intersection. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![S S](_cs.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | riin0 3892* |
Relative intersection of an empty family. (Contributed by Stefan
O'Rear, 3-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif)
![|^|_ |^|_](_capbar.gif) ![S S](_cs.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | riinm 3893* |
Relative intersection of an inhabited family. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![X X](_cx.gif) ![( (](lp.gif) ![|^|_ |^|_](_capbar.gif) ![S S](_cs.gif)
![|^|_ |^|_](_capbar.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | iinxsng 3894* |
A singleton index picks out an instance of an indexed intersection's
argument. (Contributed by NM, 15-Jan-2012.) (Proof shortened by Mario
Carneiro, 17-Nov-2016.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![|^|_
|^|_](_capbar.gif)
![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iinxprg 3895* |
Indexed intersection with an unordered pair index. (Contributed by NM,
25-Jan-2012.)
|
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![|^|_ |^|_](_capbar.gif) ![{ {](lbrace.gif) ![A A](_ca.gif)
![B B](_cb.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iunxsng 3896* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25-Jun-2016.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![U_
U_](_cupbar.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iunxsn 3897* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro,
25-Jun-2016.)
|
![( (](lp.gif)
![C C](_cc.gif) ![U_ U_](_cupbar.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![C C](_cc.gif) |
|
Theorem | iunxsngf 3898* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25-Jun-2016.) (Revised by Thierry
Arnoux, 2-May-2020.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![U_
U_](_cupbar.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iunun 3899 |
Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.)
(Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
![U_ U_](_cupbar.gif)
![( (](lp.gif)
![C C](_cc.gif)
![( (](lp.gif) ![U_ U_](_cupbar.gif)
![U_ U_](_cupbar.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | iunxun 3900 |
Separate a union in the index of an indexed union. (Contributed by NM,
26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
![U_ U_](_cupbar.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![U_ U_](_cupbar.gif) ![U_ U_](_cupbar.gif)
![C C](_cc.gif) ![) )](rp.gif) |