Type | Label | Description |
Statement |
|
Theorem | opabssxp 4701* |
An abstraction relation is a subset of a related cross product.
(Contributed by NM, 16-Jul-1995.)
|
            |
|
Theorem | brab2ga 4702* |
The law of concretion for a binary relation. See brab2a 4680 for alternate
proof. TODO: should one of them be deleted? (Contributed by Mario
Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
|
                        |
|
Theorem | optocl 4703* |
Implicit substitution of class for ordered pair. (Contributed by NM,
5-Mar-1995.)
|
     
       
  |
|
Theorem | 2optocl 4704* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
     
      
       
 
      |
|
Theorem | 3optocl 4705* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
     
      
      
     
 
          |
|
Theorem | opbrop 4706* |
Ordered pair membership in a relation. Special case. (Contributed by
NM, 5-Aug-1995.)
|
    
 
                                      
 
            |
|
Theorem | 0xp 4707 |
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
4-Jul-1994.)
|

  |
|
Theorem | csbxpg 4708 |
Distribute proper substitution through the cross product of two classes.
(Contributed by Alan Sare, 10-Nov-2012.)
|
   ![]_ ]_](_urbrack.gif)  
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | releq 4709 |
Equality theorem for the relation predicate. (Contributed by NM,
1-Aug-1994.)
|
     |
|
Theorem | releqi 4710 |
Equality inference for the relation predicate. (Contributed by NM,
8-Dec-2006.)
|
   |
|
Theorem | releqd 4711 |
Equality deduction for the relation predicate. (Contributed by NM,
8-Mar-2014.)
|
       |
|
Theorem | nfrel 4712 |
Bound-variable hypothesis builder for a relation. (Contributed by NM,
31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
     |
|
Theorem | sbcrel 4713 |
Distribute proper substitution through a relation predicate. (Contributed
by Alexander van der Vekens, 23-Jul-2017.)
|
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | relss 4714 |
Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.
(Contributed by NM, 15-Aug-1994.)
|
     |
|
Theorem | ssrel 4715* |
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33.
(Contributed by NM, 2-Aug-1994.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
 
               |
|
Theorem | eqrel 4716* |
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2-Aug-1994.)
|
   
               |
|
Theorem | ssrel2 4717* |
A subclass relationship depends only on a relation's ordered pairs.
This version of ssrel 4715 is restricted to the relation's domain.
(Contributed by Thierry Arnoux, 25-Jan-2018.)
|
   
     
       |
|
Theorem | relssi 4718* |
Inference from subclass principle for relations. (Contributed by NM,
31-Mar-1998.)
|
     
 
 |
|
Theorem | relssdv 4719* |
Deduction from subclass principle for relations. (Contributed by NM,
11-Sep-2004.)
|
      
        |
|
Theorem | eqrelriv 4720* |
Inference from extensionality principle for relations. (Contributed by
FL, 15-Oct-2012.)
|
         
   |
|
Theorem | eqrelriiv 4721* |
Inference from extensionality principle for relations. (Contributed by
NM, 17-Mar-1995.)
|
         |
|
Theorem | eqbrriv 4722* |
Inference from extensionality principle for relations. (Contributed by
NM, 12-Dec-2006.)
|
     
 |
|
Theorem | eqrelrdv 4723* |
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10-Oct-2010.)
|
          
  |
|
Theorem | eqbrrdv 4724* |
Deduction from extensionality principle for relations. (Contributed by
Mario Carneiro, 3-Jan-2017.)
|
               |
|
Theorem | eqbrrdiv 4725* |
Deduction from extensionality principle for relations. (Contributed by
Rodolfo Medina, 10-Oct-2010.)
|
           |
|
Theorem | eqrelrdv2 4726* |
A version of eqrelrdv 4723. (Contributed by Rodolfo Medina,
10-Oct-2010.)
|
            
    |
|
Theorem | ssrelrel 4727* |
A subclass relationship determined by ordered triples. Use relrelss 5156
to express the antecedent in terms of the relation predicate.
(Contributed by NM, 17-Dec-2008.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
     
            
          |
|
Theorem | eqrelrel 4728* |
Extensionality principle for ordered triples, analogous to eqrel 4716.
Use relrelss 5156 to express the antecedent in terms of the
relation
predicate. (Contributed by NM, 17-Dec-2008.)
|
  
    
                       |
|
Theorem | elrel 4729* |
A member of a relation is an ordered pair. (Contributed by NM,
17-Sep-2006.)
|
     
     |
|
Theorem | relsng 4730 |
A singleton is a relation iff it is an ordered pair. (Contributed by NM,
24-Sep-2013.) (Revised by BJ, 12-Feb-2022.)
|
         |
|
Theorem | relsnopg 4731 |
A singleton of an ordered pair is a relation. (Contributed by NM,
17-May-1998.) (Revised by BJ, 12-Feb-2022.)
|
  
       |
|
Theorem | relsn 4732 |
A singleton is a relation iff it is an ordered pair. (Contributed by
NM, 24-Sep-2013.)
|
       |
|
Theorem | relsnop 4733 |
A singleton of an ordered pair is a relation. (Contributed by NM,
17-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
      |
|
Theorem | xpss12 4734 |
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52. (Contributed by NM,
26-Aug-1995.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
    
    |
|
Theorem | xpss 4735 |
A cross product is included in the ordered pair universe. Exercise 3 of
[TakeutiZaring] p. 25. (Contributed
by NM, 2-Aug-1994.)
|
     |
|
Theorem | relxp 4736 |
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
(Contributed by NM, 2-Aug-1994.)
|
   |
|
Theorem | xpss1 4737 |
Subset relation for cross product. (Contributed by Jeff Hankins,
30-Aug-2009.)
|
       |
|
Theorem | xpss2 4738 |
Subset relation for cross product. (Contributed by Jeff Hankins,
30-Aug-2009.)
|
       |
|
Theorem | xpsspw 4739 |
A cross product is included in the power of the power of the union of
its arguments. (Contributed by NM, 13-Sep-2006.)
|
       |
|
Theorem | unixpss 4740 |
The double class union of a cross product is included in the union of its
arguments. (Contributed by NM, 16-Sep-2006.)
|
   
   |
|
Theorem | xpexg 4741 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. (Contributed
by NM, 14-Aug-1994.)
|
    
  |
|
Theorem | xpex 4742 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23.
(Contributed by NM, 14-Aug-1994.)
|
 
 |
|
Theorem | sqxpexg 4743 |
The Cartesian square of a set is a set. (Contributed by AV,
13-Jan-2020.)
|
  
  |
|
Theorem | relun 4744 |
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25. (Contributed
by NM, 12-Aug-1994.)
|
       |
|
Theorem | relin1 4745 |
The intersection with a relation is a relation. (Contributed by NM,
16-Aug-1994.)
|
     |
|
Theorem | relin2 4746 |
The intersection with a relation is a relation. (Contributed by NM,
17-Jan-2006.)
|
     |
|
Theorem | reldif 4747 |
A difference cutting down a relation is a relation. (Contributed by NM,
31-Mar-1998.)
|
     |
|
Theorem | reliun 4748 |
An indexed union is a relation iff each member of its indexed family is
a relation. (Contributed by NM, 19-Dec-2008.)
|
     |
|
Theorem | reliin 4749 |
An indexed intersection is a relation if at least one of the member of the
indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
|
     |
|
Theorem | reluni 4750* |
The union of a class is a relation iff any member is a relation.
Exercise 6 of [TakeutiZaring] p.
25 and its converse. (Contributed by
NM, 13-Aug-2004.)
|
     |
|
Theorem | relint 4751* |
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8-Mar-2014.)
|
     |
|
Theorem | rel0 4752 |
The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
|
 |
|
Theorem | relopabi 4753 |
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21-Dec-2013.)
|
      |
|
Theorem | relopab 4754 |
A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.)
(Unnecessary distinct variable restrictions were removed by Alan Sare,
9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
|
      |
|
Theorem | brabv 4755 |
If two classes are in a relationship given by an ordered-pair class
abstraction, the classes are sets. (Contributed by Alexander van der
Vekens, 5-Nov-2017.)
|
       
    |
|
Theorem | mptrel 4756 |
The maps-to notation always describes a relationship. (Contributed by
Scott Fenton, 16-Apr-2012.)
|
   |
|
Theorem | reli 4757 |
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235. (Contributed by
NM, 26-Apr-1998.) (Revised by
Mario Carneiro, 21-Dec-2013.)
|
 |
|
Theorem | rele 4758 |
The membership relation is a relation. (Contributed by NM,
26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
 |
|
Theorem | opabid2 4759* |
A relation expressed as an ordered pair abstraction. (Contributed by
NM, 11-Dec-2006.)
|
           |
|
Theorem | inopab 4760* |
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30-Sep-2002.)
|
                    |
|
Theorem | difopab 4761* |
The difference of two ordered-pair abstractions. (Contributed by Stefan
O'Rear, 17-Jan-2015.)
|
                    |
|
Theorem | inxp 4762 |
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
  
      
   |
|
Theorem | xpindi 4763 |
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26-Sep-2004.)
|
           |
|
Theorem | xpindir 4764 |
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26-Sep-2004.)
|
           |
|
Theorem | xpiindim 4765* |
Distributive law for cross product over indexed intersection.
(Contributed by Jim Kingdon, 7-Dec-2018.)
|
    
     |
|
Theorem | xpriindim 4766* |
Distributive law for cross product over relativized indexed
intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|
      
    
    |
|
Theorem | eliunxp 4767* |
Membership in a union of cross products. Analogue of elxp 4644
for
nonconstant    . (Contributed by Mario Carneiro,
29-Dec-2014.)
|
 
            
    |
|
Theorem | opeliunxp2 4768* |
Membership in a union of cross products. (Contributed by Mario
Carneiro, 14-Feb-2015.)
|
          
    |
|
Theorem | raliunxp 4769* |
Write a double restricted quantification as one universal quantifier.
In this version of ralxp 4771,    is not assumed to be constant.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
                  |
|
Theorem | rexiunxp 4770* |
Write a double restricted quantification as one universal quantifier.
In this version of rexxp 4772,    is not assumed to be constant.
(Contributed by Mario Carneiro, 14-Feb-2015.)
|
               
  |
|
Theorem | ralxp 4771* |
Universal quantification restricted to a cross product is equivalent to
a double restricted quantification. The hypothesis specifies an
implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by
Mario Carneiro, 29-Dec-2014.)
|
                |
|
Theorem | rexxp 4772* |
Existential quantification restricted to a cross product is equivalent
to a double restricted quantification. (Contributed by NM,
11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
|
             
  |
|
Theorem | djussxp 4773* |
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21-Nov-2014.)
|

   
   |
|
Theorem | ralxpf 4774* |
Version of ralxp 4771 with bound-variable hypotheses. (Contributed
by NM,
18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
                      |
|
Theorem | rexxpf 4775* |
Version of rexxp 4772 with bound-variable hypotheses. (Contributed
by NM,
19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
                   
  |
|
Theorem | iunxpf 4776* |
Indexed union on a cross product is equals a double indexed union. The
hypothesis specifies an implicit substitution. (Contributed by NM,
19-Dec-2008.)
|
           
      |
|
Theorem | opabbi2dv 4777* |
Deduce equality of a relation and an ordered-pair class builder.
Compare abbi2dv 2296. (Contributed by NM, 24-Feb-2014.)
|
               |
|
Theorem | relop 4778* |
A necessary and sufficient condition for a Kuratowski ordered pair to be
a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this
detail.)
|
          
      |
|
Theorem | ideqg 4779 |
For sets, the identity relation is the same as equality. (Contributed
by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
     |
|
Theorem | ideq 4780 |
For sets, the identity relation is the same as equality. (Contributed
by NM, 13-Aug-1995.)
|
   |
|
Theorem | ididg 4781 |
A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof
shortened by Andrew Salmon, 27-Aug-2011.)
|
   |
|
Theorem | issetid 4782 |
Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario
Carneiro, 26-Apr-2015.)
|
   |
|
Theorem | coss1 4783 |
Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|
       |
|
Theorem | coss2 4784 |
Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|
       |
|
Theorem | coeq1 4785 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
  
    |
|
Theorem | coeq2 4786 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
  
    |
|
Theorem | coeq1i 4787 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
 
   |
|
Theorem | coeq2i 4788 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
 
   |
|
Theorem | coeq1d 4789 |
Equality deduction for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
         |
|
Theorem | coeq2d 4790 |
Equality deduction for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
         |
|
Theorem | coeq12i 4791 |
Equality inference for composition of two classes. (Contributed by FL,
7-Jun-2012.)
|
 
   |
|
Theorem | coeq12d 4792 |
Equality deduction for composition of two classes. (Contributed by FL,
7-Jun-2012.)
|
           |
|
Theorem | nfco 4793 |
Bound-variable hypothesis builder for function value. (Contributed by
NM, 1-Sep-1999.)
|
         |
|
Theorem | elco 4794* |
Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
|
                      |
|
Theorem | brcog 4795* |
Ordered pair membership in a composition. (Contributed by NM,
24-Feb-2015.)
|
                   |
|
Theorem | opelco2g 4796* |
Ordered pair membership in a composition. (Contributed by NM,
27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
                      |
|
Theorem | brcogw 4797 |
Ordered pair membership in a composition. (Contributed by Thierry
Arnoux, 14-Jan-2018.)
|
   
             |
|
Theorem | eqbrrdva 4798* |
Deduction from extensionality principle for relations, given an
equivalence only on the relation's domain and range. (Contributed by
Thierry Arnoux, 28-Nov-2017.)
|
         
           |
|
Theorem | brco 4799* |
Binary relation on a composition. (Contributed by NM, 21-Sep-2004.)
(Revised by Mario Carneiro, 24-Feb-2015.)
|
               |
|
Theorem | opelco 4800* |
Ordered pair membership in a composition. (Contributed by NM,
27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
     
          |