Theorem List for Intuitionistic Logic Explorer - 4001-4100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | disjxsn 4001* |
A singleton collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj     |
|
Theorem | disjx0 4002 |
An empty collection is disjoint. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
Disj  |
|
2.1.22 Binary relations
|
|
Syntax | wbr 4003 |
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 4004 |
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 4895). (Contributed by NM, 31-Dec-1993.)
|
    
   |
|
Theorem | breq 4005 |
Equality theorem for binary relations. (Contributed by NM,
4-Jun-1995.)
|
         |
|
Theorem | breq1 4006 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
         |
|
Theorem | breq2 4007 |
Equality theorem for a binary relation. (Contributed by NM,
31-Dec-1993.)
|
         |
|
Theorem | breq12 4008 |
Equality theorem for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
           |
|
Theorem | breqi 4009 |
Equality inference for binary relations. (Contributed by NM,
19-Feb-2005.)
|
       |
|
Theorem | breq1i 4010 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
       |
|
Theorem | breq2i 4011 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
       |
|
Theorem | breq12i 4012 |
Equality inference for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
       |
|
Theorem | breq1d 4013 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
           |
|
Theorem | breqd 4014 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
           |
|
Theorem | breq2d 4015 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
           |
|
Theorem | breq12d 4016 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
             |
|
Theorem | breq123d 4017 |
Equality deduction for a binary relation. (Contributed by NM,
29-Oct-2011.)
|
               |
|
Theorem | breqdi 4018 |
Equality deduction for a binary relation. (Contributed by Thierry
Arnoux, 5-Oct-2020.)
|
           |
|
Theorem | breqan12d 4019 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
               |
|
Theorem | breqan12rd 4020 |
Equality deduction for a binary relation. (Contributed by NM,
8-Feb-1996.)
|
               |
|
Theorem | eqnbrtrd 4021 |
Substitution of equal classes into the negation of a binary relation.
(Contributed by Glauco Siliprandi, 3-Jan-2021.)
|
      
    |
|
Theorem | nbrne1 4022 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
      
  |
|
Theorem | nbrne2 4023 |
Two classes are different if they don't have the same relationship to a
third class. (Contributed by NM, 3-Jun-2012.)
|
      
  |
|
Theorem | eqbrtri 4024 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
     |
|
Theorem | eqbrtrd 4025 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 8-Oct-1999.)
|
           |
|
Theorem | eqbrtrri 4026 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
     |
|
Theorem | eqbrtrrd 4027 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
           |
|
Theorem | breqtri 4028 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
     |
|
Theorem | breqtrd 4029 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
           |
|
Theorem | breqtrri 4030 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 5-Aug-1993.)
|
     |
|
Theorem | breqtrrd 4031 |
Substitution of equal classes into a binary relation. (Contributed by
NM, 24-Oct-1999.)
|
           |
|
Theorem | 3brtr3i 4032 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
     |
|
Theorem | 3brtr4i 4033 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 11-Aug-1999.)
|
     |
|
Theorem | 3brtr3d 4034 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 18-Oct-1999.)
|
             |
|
Theorem | 3brtr4d 4035 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 21-Feb-2005.)
|
             |
|
Theorem | 3brtr3g 4036 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
         |
|
Theorem | 3brtr4g 4037 |
Substitution of equality into both sides of a binary relation.
(Contributed by NM, 16-Jan-1997.)
|
         |
|
Theorem | eqbrtrid 4038 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
         |
|
Theorem | eqbrtrrid 4039 |
B chained equality inference for a binary relation. (Contributed by NM,
17-Sep-2004.)
|
         |
|
Theorem | breqtrid 4040 |
B chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
         |
|
Theorem | breqtrrid 4041 |
B chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
         |
|
Theorem | eqbrtrdi 4042 |
A chained equality inference for a binary relation. (Contributed by NM,
12-Oct-1999.)
|
         |
|
Theorem | eqbrtrrdi 4043 |
A chained equality inference for a binary relation. (Contributed by NM,
4-Jan-2006.)
|
         |
|
Theorem | breqtrdi 4044 |
A chained equality inference for a binary relation. (Contributed by NM,
11-Oct-1999.)
|
         |
|
Theorem | breqtrrdi 4045 |
A chained equality inference for a binary relation. (Contributed by NM,
24-Apr-2005.)
|
         |
|
Theorem | ssbrd 4046 |
Deduction from a subclass relationship of binary relations.
(Contributed by NM, 30-Apr-2004.)
|
           |
|
Theorem | ssbri 4047 |
Inference from a subclass relationship of binary relations.
(Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro,
8-Feb-2015.)
|
       |
|
Theorem | nfbrd 4048 |
Deduction version of bound-variable hypothesis builder nfbr 4049.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
            
     |
|
Theorem | nfbr 4049 |
Bound-variable hypothesis builder for binary relation. (Contributed by
NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
          |
|
Theorem | brab1 4050* |
Relationship between a binary relation and a class abstraction.
(Contributed by Andrew Salmon, 8-Jul-2011.)
|
         |
|
Theorem | br0 4051 |
The empty binary relation never holds. (Contributed by NM,
23-Aug-2018.)
|
   |
|
Theorem | brne0 4052 |
If two sets are in a binary relation, the relation cannot be empty. In
fact, the relation is also inhabited, as seen at brm 4053.
(Contributed by
Alexander van der Vekens, 7-Jul-2018.)
|
     |
|
Theorem | brm 4053* |
If two sets are in a binary relation, the relation is inhabited.
(Contributed by Jim Kingdon, 31-Dec-2023.)
|
      |
|
Theorem | brun 4054 |
The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|
             |
|
Theorem | brin 4055 |
The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|
             |
|
Theorem | brdif 4056 |
The difference of two binary relations. (Contributed by Scott Fenton,
11-Apr-2011.)
|
             |
|
Theorem | sbcbrg 4057 |
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)    |
|
Theorem | sbcbr12g 4058* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
    ![]. ].](_drbrack.gif)     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
|
Theorem | sbcbr1g 4059* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
    ![]. ].](_drbrack.gif)     ![]_ ]_](_urbrack.gif)      |
|
Theorem | sbcbr2g 4060* |
Move substitution in and out of a binary relation. (Contributed by NM,
13-Dec-2005.)
|
    ![]. ].](_drbrack.gif)       ![]_ ]_](_urbrack.gif)    |
|
Theorem | brralrspcev 4061* |
Restricted existential specialization with a restricted universal
quantifier over a relation, closed form. (Contributed by AV,
20-Aug-2022.)
|
            |
|
Theorem | brimralrspcev 4062* |
Restricted existential specialization with a restricted universal
quantifier over an implication with a relation in the antecedent, closed
form. (Contributed by AV, 20-Aug-2022.)
|
          
         |
|
2.1.23 Ordered-pair class abstractions (class
builders)
|
|
Syntax | copab 4063 |
Extend class notation to include ordered-pair class abstraction (class
builder).
|
      |
|
Syntax | cmpt 4064 |
Extend the definition of a class to include maps-to notation for defining
a function via a rule.
|

  |
|
Definition | df-opab 4065* |
Define the class abstraction of a collection of ordered pairs.
Definition 3.3 of [Monk1] p. 34. Usually
and are distinct,
although the definition doesn't strictly require it. The brace notation
is called "class abstraction" by Quine; it is also (more
commonly)
called a "class builder" in the literature. (Contributed by
NM,
4-Jul-1994.)
|
     
           |
|
Definition | df-mpt 4066* |
Define maps-to notation for defining a function via a rule. Read as
"the function defined by the map from (in ) to
   ". The class expression is the value of the function
at and normally
contains the variable .
Similar to the
definition of mapping in [ChoquetDD]
p. 2. (Contributed by NM,
17-Feb-2008.)
|
 
    
   |
|
Theorem | opabss 4067* |
The collection of ordered pairs in a class is a subclass of it.
(Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon,
9-Jul-2011.)
|
      
 |
|
Theorem | opabbid 4068 |
Equivalent wff's yield equal ordered-pair class abstractions (deduction
form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew
Salmon, 9-Jul-2011.)
|
                     |
|
Theorem | opabbidv 4069* |
Equivalent wff's yield equal ordered-pair class abstractions (deduction
form). (Contributed by NM, 15-May-1995.)
|
                 |
|
Theorem | opabbii 4070 |
Equivalent wff's yield equal class abstractions. (Contributed by NM,
15-May-1995.)
|
             |
|
Theorem | nfopab 4071* |
Bound-variable hypothesis builder for class abstraction. (Contributed
by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by
Andrew Salmon, 11-Jul-2011.)
|
          |
|
Theorem | nfopab1 4072 |
The first abstraction variable in an ordered-pair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
        |
|
Theorem | nfopab2 4073 |
The second abstraction variable in an ordered-pair class abstraction
(class builder) is effectively not free. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
        |
|
Theorem | cbvopab 4074* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
14-Sep-2003.)
|
                         |
|
Theorem | cbvopabv 4075* |
Rule used to change bound variables in an ordered-pair class
abstraction, using implicit substitution. (Contributed by NM,
15-Oct-1996.)
|
                 |
|
Theorem | cbvopab1 4076* |
Change first bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by
Mario Carneiro, 14-Oct-2016.)
|
    
              |
|
Theorem | cbvopab2 4077* |
Change second bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 22-Aug-2013.)
|
    
              |
|
Theorem | cbvopab1s 4078* |
Change first bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 31-Jul-2003.)
|
           ![] ]](rbrack.gif)   |
|
Theorem | cbvopab1v 4079* |
Rule used to change the first bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|
               |
|
Theorem | cbvopab2v 4080* |
Rule used to change the second bound variable in an ordered pair
abstraction, using implicit substitution. (Contributed by NM,
2-Sep-1999.)
|
               |
|
Theorem | csbopabg 4081* |
Move substitution into a class abstraction. (Contributed by NM,
6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
   ![]_ ]_](_urbrack.gif)            ![]. ].](_drbrack.gif)    |
|
Theorem | unopab 4082 |
Union of two ordered pair class abstractions. (Contributed by NM,
30-Sep-2002.)
|
                    |
|
Theorem | mpteq12f 4083 |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
  
  
     |
|
Theorem | mpteq12dva 4084* |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 26-Jan-2017.)
|
      
      |
|
Theorem | mpteq12dv 4085* |
An equality inference for the maps-to notation. (Contributed by NM,
24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
|
           |
|
Theorem | mpteq12 4086* |
An equality theorem for the maps-to notation. (Contributed by NM,
16-Dec-2013.)
|
          |
|
Theorem | mpteq1 4087* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
  

   |
|
Theorem | mpteq1d 4088* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
   
     |
|
Theorem | mpteq2ia 4089 |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
  


  |
|
Theorem | mpteq2i 4090 |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
     |
|
Theorem | mpteq12i 4091 |
An equality inference for the maps-to notation. (Contributed by Scott
Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
|
 

  |
|
Theorem | mpteq2da 4092 |
Slightly more general equality inference for the maps-to notation.
(Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro,
16-Dec-2013.)
|
      
      |
|
Theorem | mpteq2dva 4093* |
Slightly more general equality inference for the maps-to notation.
(Contributed by Scott Fenton, 25-Apr-2012.)
|
     
     |
|
Theorem | mpteq2dv 4094* |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 23-Aug-2014.)
|
   
     |
|
Theorem | nfmpt 4095* |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by NM, 20-Feb-2013.)
|
         |
|
Theorem | nfmpt1 4096 |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by FL, 17-Feb-2008.)
|
     |
|
Theorem | cbvmptf 4097* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version has bound-variable hypotheses in place of
distinct variable conditions. (Contributed by Thierry Arnoux,
9-Mar-2017.)
|
        
  
   |
|
Theorem | cbvmpt 4098* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version has bound-variable hypotheses in place of
distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
|
    
      |
|
Theorem | cbvmptv 4099* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
|
  

   |
|
Theorem | mptv 4100* |
Function with universal domain in maps-to notation. (Contributed by NM,
16-Aug-2013.)
|
 
      |