Theorem List for Intuitionistic Logic Explorer - 3801-3900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | iundif2ss 3801* |
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 3802* |
Rearrange indexed unions over intersection. (Contributed by NM,
18-Dec-2008.)
|

        |
|
Theorem | iindif2m 3803* |
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 3804* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
          |
|
Theorem | iinin1m 3805* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
          |
|
Theorem | elriin 3806* |
Elementhood in a relative intersection. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
   
     |
|
Theorem | riin0 3807* |
Relative intersection of an empty family. (Contributed by Stefan
O'Rear, 3-Apr-2015.)
|
 
    |
|
Theorem | riinm 3808* |
Relative intersection of an inhabited family. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
       
   |
|
Theorem | iinxsng 3809* |
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 3810* |
Indexed intersection with an unordered pair index. (Contributed by NM,
25-Jan-2012.)
|
  
      
 
    |
|
Theorem | iunxsng 3811* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25-Jun-2016.)
|
  
      |
|
Theorem | iunxsn 3812* |
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 | iunxsngf 3813* |
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.)
|
  
        |
|
Theorem | iunun 3814 |
Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.)
(Proof shortened by Mario Carneiro, 17-Nov-2016.)
|



 
   |
|
Theorem | iunxun 3815 |
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 3816* |
Separate an indexed union in the index of an indexed union.
(Contributed by Mario Carneiro, 5-Dec-2016.)
|

  
 |
|
Theorem | iinuniss 3817* |
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 3818* |
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 3819 |
Subclass relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
  
  |
|
Theorem | pwssb 3820* |
Two ways to express a collection of subclasses. (Contributed by NM,
19-Jul-2006.)
|
     |
|
Theorem | elpwpw 3821 |
Characterization of the elements of a double power class: they are exactly
the sets whose union is included in that class. (Contributed by BJ,
29-Apr-2021.)
|
  
     |
|
Theorem | pwpwab 3822* |
The double power class written as a class abstraction: the class of sets
whose union is included in the given class. (Contributed by BJ,
29-Apr-2021.)
|
  
   |
|
Theorem | pwpwssunieq 3823* |
The class of sets whose union is equal to a given class is included in
the double power class of that class. (Contributed by BJ,
29-Apr-2021.)
|
 
    |
|
Theorem | elpwuni 3824 |
Relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
       |
|
Theorem | iinpw 3825* |
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 3826* |
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 3827* |
Relative intersection of an inhabited class. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
   
       |
|
2.1.21 Disjointness
|
|
Syntax | wdisj 3828 |
Extend wff notation to include the statement that a family of classes
   , for , is a disjoint family.
|
Disj  |
|
Definition | df-disj 3829* |
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 3830* |
Alternate definition for disjoint classes. (Contributed by NM,
17-Jun-2017.)
|
Disj
    
   |
|
Theorem | disjss2 3831 |
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 3832 |
Equality theorem for disjoint collection. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
  Disj
Disj
   |
|
Theorem | disjeq2dv 3833* |
Equality deduction for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
     Disj Disj    |
|
Theorem | disjss1 3834* |
A subset of a disjoint collection is disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
 Disj
Disj    |
|
Theorem | disjeq1 3835* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
 Disj
Disj
   |
|
Theorem | disjeq1d 3836* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
   Disj Disj    |
|
Theorem | disjeq12d 3837* |
Equality theorem for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
     Disj
Disj    |
|
Theorem | cbvdisj 3838* |
Change bound variables in a disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
    
 Disj
Disj   |
|
Theorem | cbvdisjv 3839* |
Change bound variables in a disjoint collection. (Contributed by Mario
Carneiro, 11-Dec-2016.)
|
  Disj Disj   |
|
Theorem | nfdisjv 3840* |
Bound-variable hypothesis builder for disjoint collection. (Contributed
by Jim Kingdon, 19-Aug-2018.)
|
     Disj  |
|
Theorem | nfdisj1 3841 |
Bound-variable hypothesis builder for disjoint collection. (Contributed
by Mario Carneiro, 14-Nov-2016.)
|
 Disj
 |
|
Theorem | disjnim 3842* |
If a collection    for is disjoint, then pairs are
disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by
Jim Kingdon, 6-Oct-2022.)
|
  Disj    
    |
|
Theorem | disjnims 3843* |
If a collection    for is disjoint, then pairs are
disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by
Jim Kingdon, 7-Oct-2022.)
|
Disj
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
|
Theorem | disji2 3844* |
Property of a disjoint collection: if    and
   , and , then and
are disjoint.
(Contributed by Mario Carneiro, 14-Nov-2016.)
|
  
  Disj
       |
|
Theorem | invdisj 3845* |
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 | disjiun 3846* |
A disjoint collection yields disjoint indexed unions for disjoint index
sets. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario
Carneiro, 14-Nov-2016.)
|
 Disj
      
 
  |
|
Theorem | sndisj 3847 |
Any collection of singletons is disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
Disj    |
|
Theorem | 0disj 3848 |
Any collection of empty sets is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj  |
|
Theorem | disjxsn 3849* |
A singleton collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj     |
|
Theorem | disjx0 3850 |
An empty collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj  |
|
2.1.22 Binary relations
|
|
Syntax | wbr 3851 |
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 3852 |
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 4714). (Contributed by NM, 31-Dec-1993.)
|
    
   |
|
Theorem | breq 3853 |
Equality theorem for binary relations. (Contributed by NM,
4-Jun-1995.)
|
         |
|
Theorem | breq1 3854 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
         |
|
Theorem | breq2 3855 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
         |
|
Theorem | breq12 3856 |
Equality theorem for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
           |
|
Theorem | breqi 3857 |
Equality inference for binary relations. (Contributed by NM,
19-Feb-2005.)
|
       |
|
Theorem | breq1i 3858 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
       |
|
Theorem | breq2i 3859 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
       |
|
Theorem | breq12i 3860 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
       |
|
Theorem | breq1d 3861 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
           |
|
Theorem | breqd 3862 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
           |
|
Theorem | breq2d 3863 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
           |
|
Theorem | breq12d 3864 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
             |
|
Theorem | breq123d 3865 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
               |
|
Theorem | breqan12d 3866 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
               |
|
Theorem | breqan12rd 3867 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
               |
|
Theorem | nbrne1 3868 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
      
  |
|
Theorem | nbrne2 3869 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
      
  |
|
Theorem | eqbrtri 3870 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
     |
|
Theorem | eqbrtrd 3871 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 8-Oct-1999.)
|
           |
|
Theorem | eqbrtrri 3872 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
     |
|
Theorem | eqbrtrrd 3873 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
           |
|
Theorem | breqtri 3874 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
     |
|
Theorem | breqtrd 3875 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
           |
|
Theorem | breqtrri 3876 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
     |
|
Theorem | breqtrrd 3877 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
           |
|
Theorem | 3brtr3i 3878 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
     |
|
Theorem | 3brtr4i 3879 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
     |
|
Theorem | 3brtr3d 3880 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 18-Oct-1999.)
|
             |
|
Theorem | 3brtr4d 3881 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 21-Feb-2005.)
|
             |
|
Theorem | 3brtr3g 3882 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
         |
|
Theorem | 3brtr4g 3883 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
         |
|
Theorem | syl5eqbr 3884 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
         |
|
Theorem | syl5eqbrr 3885 |
B chained equality inference for a binary relation. (Contributed by NM,
17-Sep-2004.)
|
         |
|
Theorem | syl5breq 3886 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
         |
|
Theorem | syl5breqr 3887 |
B chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
         |
|
Theorem | syl6eqbr 3888 |
A chained equality inference for a binary relation. (Contributed by NM,
12-Oct-1999.)
|
         |
|
Theorem | syl6eqbrr 3889 |
A chained equality inference for a binary relation. (Contributed by NM,
4-Jan-2006.)
|
         |
|
Theorem | syl6breq 3890 |
A chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
         |
|
Theorem | syl6breqr 3891 |
A chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
         |
|
Theorem | ssbrd 3892 |
Deduction from a subclass relationship of binary relations.
(Contributed by NM, 30-Apr-2004.)
|
           |
|
Theorem | ssbri 3893 |
Inference from a subclass relationship of binary relations.
(Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro,
8-Feb-2015.)
|
       |
|
Theorem | nfbrd 3894 |
Deduction version of bound-variable hypothesis builder nfbr 3895.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
            
     |
|
Theorem | nfbr 3895 |
Bound-variable hypothesis builder for binary relation. (Contributed by
NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
          |
|
Theorem | brab1 3896* |
Relationship between a binary relation and a class abstraction.
(Contributed by Andrew Salmon, 8-Jul-2011.)
|
         |
|
Theorem | brun 3897 |
The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|
             |
|
Theorem | brin 3898 |
The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|
             |
|
Theorem | brdif 3899 |
The difference of two binary relations. (Contributed by Scott Fenton,
11-Apr-2011.)
|
             |
|
Theorem | sbcbrg 3900 |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
    ![]. ].](_drbrack.gif)     ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |