Theorem List for Intuitionistic Logic Explorer - 3701-3800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | iuneq1d 3701* |
Equality theorem for indexed union, deduction version. (Contributed by
Drahflow, 22-Oct-2015.)
|
|
|
Theorem | iuneq12d 3702* |
Equality deduction for indexed union, deduction version. (Contributed
by Drahflow, 22-Oct-2015.)
|
|
|
Theorem | iuneq2d 3703* |
Equality deduction for indexed union. (Contributed by Drahflow,
22-Oct-2015.)
|
|
|
Theorem | nfiunxy 3704* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
|
|
Theorem | nfiinxy 3705* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
|
|
Theorem | nfiunya 3706* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
|
|
Theorem | nfiinya 3707* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
|
|
Theorem | nfiu1 3708 |
Bound-variable hypothesis builder for indexed union. (Contributed by
NM, 12-Oct-2003.)
|
|
|
Theorem | nfii1 3709 |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by NM, 15-Oct-2003.)
|
|
|
Theorem | dfiun2g 3710* |
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.)
|
|
|
Theorem | dfiin2g 3711* |
Alternate definition of indexed intersection when is a set.
(Contributed by Jeff Hankins, 27-Aug-2009.)
|
|
|
Theorem | dfiun2 3712* |
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.)
|
|
|
Theorem | dfiin2 3713* |
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.)
|
|
|
Theorem | dfiunv2 3714* |
Define double indexed union. (Contributed by FL, 6-Nov-2013.)
|
|
|
Theorem | cbviun 3715* |
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.)
|
|
|
Theorem | cbviin 3716* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | cbviunv 3717* |
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.)
|
|
|
Theorem | cbviinv 3718* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.)
|
|
|
Theorem | iunss 3719* |
Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | ssiun 3720* |
Subset implication for an indexed union. (Contributed by NM,
3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | ssiun2 3721 |
Identity law for subset of an indexed union. (Contributed by NM,
12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | ssiun2s 3722* |
Subset relationship for an indexed union. (Contributed by NM,
26-Oct-2003.)
|
|
|
Theorem | iunss2 3723* |
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 3632. (Contributed by NM, 9-Dec-2004.)
|
|
|
Theorem | iunab 3724* |
The indexed union of a class abstraction. (Contributed by NM,
27-Dec-2004.)
|
|
|
Theorem | iunrab 3725* |
The indexed union of a restricted class abstraction. (Contributed by
NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|
|
|
Theorem | iunxdif2 3726* |
Indexed union with a class difference as its index. (Contributed by NM,
10-Dec-2004.)
|
|
|
Theorem | ssiinf 3727 |
Subset theorem for an indexed intersection. (Contributed by FL,
15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | ssiin 3728* |
Subset theorem for an indexed intersection. (Contributed by NM,
15-Oct-2003.)
|
|
|
Theorem | iinss 3729* |
Subset implication for an indexed intersection. (Contributed by NM,
15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | iinss2 3730 |
An indexed intersection is included in any of its members. (Contributed
by FL, 15-Oct-2012.)
|
|
|
Theorem | uniiun 3731* |
Class union in terms of indexed union. Definition in [Stoll] p. 43.
(Contributed by NM, 28-Jun-1998.)
|
|
|
Theorem | intiin 3732* |
Class intersection in terms of indexed intersection. Definition in
[Stoll] p. 44. (Contributed by NM,
28-Jun-1998.)
|
|
|
Theorem | iunid 3733* |
An indexed union of singletons recovers the index set. (Contributed by
NM, 6-Sep-2005.)
|
|
|
Theorem | iun0 3734 |
An indexed union of the empty set is empty. (Contributed by NM,
26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | 0iun 3735 |
An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | 0iin 3736 |
An empty indexed intersection is the universal class. (Contributed by
NM, 20-Oct-2005.)
|
|
|
Theorem | viin 3737* |
Indexed intersection with a universal index class. (Contributed by NM,
11-Sep-2008.)
|
|
|
Theorem | iunn0m 3738* |
There is an inhabited class in an indexed collection iff the
indexed union of them is inhabited. (Contributed by Jim Kingdon,
16-Aug-2018.)
|
|
|
Theorem | iinab 3739* |
Indexed intersection of a class builder. (Contributed by NM,
6-Dec-2011.)
|
|
|
Theorem | iinrabm 3740* |
Indexed intersection of a restricted class builder. (Contributed by Jim
Kingdon, 16-Aug-2018.)
|
|
|
Theorem | iunin2 3741* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3731 to recover
Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
|
|
|
Theorem | iunin1 3742* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3731 to recover
Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
|
|
|
Theorem | iundif2ss 3743* |
Indexed union of class difference. Compare to theorem "De Morgan's
laws" in [Enderton] p. 31.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
|
|
Theorem | 2iunin 3744* |
Rearrange indexed unions over intersection. (Contributed by NM,
18-Dec-2008.)
|
|
|
Theorem | iindif2m 3745* |
Indexed intersection of class difference. Compare to Theorem "De
Morgan's laws" in [Enderton] p.
31. (Contributed by Jim Kingdon,
17-Aug-2018.)
|
|
|
Theorem | iinin2m 3746* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
|
|
Theorem | iinin1m 3747* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
|
|
Theorem | elriin 3748* |
Elementhood in a relative intersection. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
|
|
Theorem | riin0 3749* |
Relative intersection of an empty family. (Contributed by Stefan
O'Rear, 3-Apr-2015.)
|
|
|
Theorem | riinm 3750* |
Relative intersection of an inhabited family. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
|
|
Theorem | iinxsng 3751* |
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.)
|
|
|
Theorem | iinxprg 3752* |
Indexed intersection with an unordered pair index. (Contributed by NM,
25-Jan-2012.)
|
|
|
Theorem | iunxsng 3753* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25-Jun-2016.)
|
|
|
Theorem | iunxsn 3754* |
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.)
|
|
|
Theorem | iunun 3755 |
Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.)
(Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
|
|
Theorem | iunxun 3756 |
Separate a union in the index of an indexed union. (Contributed by NM,
26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
|
|
Theorem | iunxiun 3757* |
Separate an indexed union in the index of an indexed union.
(Contributed by Mario Carneiro, 5-Dec-2016.)
|
|
|
Theorem | iinuniss 3758* |
A relationship involving union and indexed intersection. Exercise 23 of
[Enderton] p. 33 but with equality
changed to subset. (Contributed by
Jim Kingdon, 19-Aug-2018.)
|
|
|
Theorem | iununir 3759* |
A relationship involving union and indexed union. Exercise 25 of
[Enderton] p. 33 but with biconditional
changed to implication.
(Contributed by Jim Kingdon, 19-Aug-2018.)
|
|
|
Theorem | sspwuni 3760 |
Subclass relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
|
|
Theorem | pwssb 3761* |
Two ways to express a collection of subclasses. (Contributed by NM,
19-Jul-2006.)
|
|
|
Theorem | elpwuni 3762 |
Relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
|
|
Theorem | iinpw 3763* |
The power class of an intersection in terms of indexed intersection.
Exercise 24(a) of [Enderton] p. 33.
(Contributed by NM,
29-Nov-2003.)
|
|
|
Theorem | iunpwss 3764* |
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, 25-Nov-2003.)
|
|
|
Theorem | rintm 3765* |
Relative intersection of an inhabited class. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
|
|
2.1.21 Disjointness
|
|
Syntax | wdisj 3766 |
Extend wff notation to include the statement that a family of classes
, for , is a disjoint family.
|
Disj |
|
Definition | df-disj 3767* |
A collection of classes is disjoint when for each element
, it is in for at most
one . (Contributed by
Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.)
|
Disj
|
|
Theorem | dfdisj2 3768* |
Alternate definition for disjoint classes. (Contributed by NM,
17-Jun-2017.)
|
Disj
|
|
Theorem | disjss2 3769 |
If each element of a collection is contained in a disjoint collection,
the original collection is also disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj
Disj |
|
Theorem | disjeq2 3770 |
Equality theorem for disjoint collection. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj
Disj
|
|
Theorem | disjeq2dv 3771* |
Equality deduction for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj Disj |
|
Theorem | disjss1 3772* |
A subset of a disjoint collection is disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj
Disj |
|
Theorem | disjeq1 3773* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj
Disj
|
|
Theorem | disjeq1d 3774* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj Disj |
|
Theorem | disjeq12d 3775* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj
Disj |
|
Theorem | cbvdisj 3776* |
Change bound variables in a disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj
Disj |
|
Theorem | cbvdisjv 3777* |
Change bound variables in a disjoint collection. (Contributed by Mario
Carneiro, 11-Dec-2016.)
|
Disj Disj |
|
Theorem | nfdisjv 3778* |
Bound-variable hypothesis builder for disjoint collection. (Contributed
by Jim Kingdon, 19-Aug-2018.)
|
Disj |
|
Theorem | nfdisj1 3779 |
Bound-variable hypothesis builder for disjoint collection. (Contributed
by Mario Carneiro, 14-Nov-2016.)
|
Disj
|
|
Theorem | invdisj 3780* |
If there is a function such that for all
, then the sets for distinct
are
disjoint. (Contributed by Mario Carneiro, 10-Dec-2016.)
|
Disj |
|
Theorem | sndisj 3781 |
Any collection of singletons is disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj |
|
Theorem | 0disj 3782 |
Any collection of empty sets is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj |
|
Theorem | disjxsn 3783* |
A singleton collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj |
|
Theorem | disjx0 3784 |
An empty collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj |
|
2.1.22 Binary relations
|
|
Syntax | wbr 3785 |
Extend wff notation to include the general binary relation predicate.
Note that the syntax is simply three class symbols in a row. Since binary
relations are the only possible wff expressions consisting of three class
expressions in a row, the syntax is unambiguous.
|
|
|
Definition | df-br 3786 |
Define a general binary relation. Note that the syntax is simply three
class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29
generalized to arbitrary classes. This definition of relations is
well-defined, although not very meaningful, when classes and/or
are proper
classes (i.e. are not sets). On the other hand, we often
find uses for this definition when is a proper class (see for
example iprc 4618). (Contributed by NM, 31-Dec-1993.)
|
|
|
Theorem | breq 3787 |
Equality theorem for binary relations. (Contributed by NM,
4-Jun-1995.)
|
|
|
Theorem | breq1 3788 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
|
|
Theorem | breq2 3789 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
|
|
Theorem | breq12 3790 |
Equality theorem for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breqi 3791 |
Equality inference for binary relations. (Contributed by NM,
19-Feb-2005.)
|
|
|
Theorem | breq1i 3792 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breq2i 3793 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breq12i 3794 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
|
|
Theorem | breq1d 3795 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breqd 3796 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
|
|
Theorem | breq2d 3797 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|
|
Theorem | breq12d 3798 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
|
|
Theorem | breq123d 3799 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
|
|
Theorem | breqan12d 3800 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
|