Type  Label  Description 
Statement 

Theorem  brab2ga 4501* 
The law of concretion for a binary relation. See brab2a 4479 for alternate
proof. TODO: should one of them be deleted? (Contributed by Mario
Carneiro, 28Apr2015.) (Proof modification is discouraged.)



Theorem  optocl 4502* 
Implicit substitution of class for ordered pair. (Contributed by NM,
5Mar1995.)



Theorem  2optocl 4503* 
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12Mar1995.)



Theorem  3optocl 4504* 
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12Mar1995.)



Theorem  opbrop 4505* 
Ordered pair membership in a relation. Special case. (Contributed by
NM, 5Aug1995.)



Theorem  0xp 4506 
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
4Jul1994.)



Theorem  csbxpg 4507 
Distribute proper substitution through the cross product of two classes.
(Contributed by Alan Sare, 10Nov2012.)



Theorem  releq 4508 
Equality theorem for the relation predicate. (Contributed by NM,
1Aug1994.)



Theorem  releqi 4509 
Equality inference for the relation predicate. (Contributed by NM,
8Dec2006.)



Theorem  releqd 4510 
Equality deduction for the relation predicate. (Contributed by NM,
8Mar2014.)



Theorem  nfrel 4511 
Boundvariable hypothesis builder for a relation. (Contributed by NM,
31Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  sbcrel 4512 
Distribute proper substitution through a relation predicate. (Contributed
by Alexander van der Vekens, 23Jul2017.)



Theorem  relss 4513 
Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.
(Contributed by NM, 15Aug1994.)



Theorem  ssrel 4514* 
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33.
(Contributed by NM, 2Aug1994.)
(Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  eqrel 4515* 
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2Aug1994.)



Theorem  ssrel2 4516* 
A subclass relationship depends only on a relation's ordered pairs.
This version of ssrel 4514 is restricted to the relation's domain.
(Contributed by Thierry Arnoux, 25Jan2018.)



Theorem  relssi 4517* 
Inference from subclass principle for relations. (Contributed by NM,
31Mar1998.)



Theorem  relssdv 4518* 
Deduction from subclass principle for relations. (Contributed by NM,
11Sep2004.)



Theorem  eqrelriv 4519* 
Inference from extensionality principle for relations. (Contributed by
FL, 15Oct2012.)



Theorem  eqrelriiv 4520* 
Inference from extensionality principle for relations. (Contributed by
NM, 17Mar1995.)



Theorem  eqbrriv 4521* 
Inference from extensionality principle for relations. (Contributed by
NM, 12Dec2006.)



Theorem  eqrelrdv 4522* 
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10Oct2010.)



Theorem  eqbrrdv 4523* 
Deduction from extensionality principle for relations. (Contributed by
Mario Carneiro, 3Jan2017.)



Theorem  eqbrrdiv 4524* 
Deduction from extensionality principle for relations. (Contributed by
Rodolfo Medina, 10Oct2010.)



Theorem  eqrelrdv2 4525* 
A version of eqrelrdv 4522. (Contributed by Rodolfo Medina,
10Oct2010.)



Theorem  ssrelrel 4526* 
A subclass relationship determined by ordered triples. Use relrelss 4944
to express the antecedent in terms of the relation predicate.
(Contributed by NM, 17Dec2008.) (Proof shortened by Andrew Salmon,
27Aug2011.)



Theorem  eqrelrel 4527* 
Extensionality principle for ordered triples, analogous to eqrel 4515.
Use relrelss 4944 to express the antecedent in terms of the
relation
predicate. (Contributed by NM, 17Dec2008.)



Theorem  elrel 4528* 
A member of a relation is an ordered pair. (Contributed by NM,
17Sep2006.)



Theorem  relsng 4529 
A singleton is a relation iff it is an ordered pair. (Contributed by NM,
24Sep2013.) (Revised by BJ, 12Feb2022.)



Theorem  relsnopg 4530 
A singleton of an ordered pair is a relation. (Contributed by NM,
17May1998.) (Revised by BJ, 12Feb2022.)



Theorem  relsn 4531 
A singleton is a relation iff it is an ordered pair. (Contributed by
NM, 24Sep2013.)



Theorem  relsnop 4532 
A singleton of an ordered pair is a relation. (Contributed by NM,
17May1998.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  xpss12 4533 
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52. (Contributed by NM,
26Aug1995.) (Proof shortened by
Andrew Salmon, 27Aug2011.)



Theorem  xpss 4534 
A cross product is included in the ordered pair universe. Exercise 3 of
[TakeutiZaring] p. 25. (Contributed
by NM, 2Aug1994.)



Theorem  relxp 4535 
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
(Contributed by NM, 2Aug1994.)



Theorem  xpss1 4536 
Subset relation for cross product. (Contributed by Jeff Hankins,
30Aug2009.)



Theorem  xpss2 4537 
Subset relation for cross product. (Contributed by Jeff Hankins,
30Aug2009.)



Theorem  xpsspw 4538 
A cross product is included in the power of the power of the union of
its arguments. (Contributed by NM, 13Sep2006.)



Theorem  unixpss 4539 
The double class union of a cross product is included in the union of its
arguments. (Contributed by NM, 16Sep2006.)



Theorem  xpexg 4540 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. (Contributed
by NM, 14Aug1994.)



Theorem  xpex 4541 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23.
(Contributed by NM, 14Aug1994.)



Theorem  relun 4542 
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25. (Contributed
by NM, 12Aug1994.)



Theorem  relin1 4543 
The intersection with a relation is a relation. (Contributed by NM,
16Aug1994.)



Theorem  relin2 4544 
The intersection with a relation is a relation. (Contributed by NM,
17Jan2006.)



Theorem  reldif 4545 
A difference cutting down a relation is a relation. (Contributed by NM,
31Mar1998.)



Theorem  reliun 4546 
An indexed union is a relation iff each member of its indexed family is
a relation. (Contributed by NM, 19Dec2008.)



Theorem  reliin 4547 
An indexed intersection is a relation if at least one of the member of the
indexed family is a relation. (Contributed by NM, 8Mar2014.)



Theorem  reluni 4548* 
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, 13Aug2004.)



Theorem  relint 4549* 
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8Mar2014.)



Theorem  rel0 4550 
The empty set is a relation. (Contributed by NM, 26Apr1998.)



Theorem  relopabi 4551 
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21Dec2013.)



Theorem  relopab 4552 
A class of ordered pairs is a relation. (Contributed by NM, 8Mar1995.)
(Unnecessary distinct variable restrictions were removed by Alan Sare,
9Jul2013.) (Proof shortened by Mario Carneiro, 21Dec2013.)



Theorem  reli 4553 
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235. (Contributed by
NM, 26Apr1998.) (Revised by
Mario Carneiro, 21Dec2013.)



Theorem  rele 4554 
The membership relation is a relation. (Contributed by NM,
26Apr1998.) (Revised by Mario Carneiro, 21Dec2013.)



Theorem  opabid2 4555* 
A relation expressed as an ordered pair abstraction. (Contributed by
NM, 11Dec2006.)



Theorem  inopab 4556* 
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30Sep2002.)



Theorem  difopab 4557* 
The difference of two orderedpair abstractions. (Contributed by Stefan
O'Rear, 17Jan2015.)



Theorem  inxp 4558 
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (Contributed by NM, 3Aug1994.) (Proof shortened by Andrew
Salmon, 27Aug2011.)



Theorem  xpindi 4559 
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26Sep2004.)



Theorem  xpindir 4560 
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26Sep2004.)



Theorem  xpiindim 4561* 
Distributive law for cross product over indexed intersection.
(Contributed by Jim Kingdon, 7Dec2018.)



Theorem  xpriindim 4562* 
Distributive law for cross product over relativized indexed
intersection. (Contributed by Jim Kingdon, 7Dec2018.)



Theorem  eliunxp 4563* 
Membership in a union of cross products. Analogue of elxp 4445
for
nonconstant . (Contributed by Mario Carneiro,
29Dec2014.)



Theorem  opeliunxp2 4564* 
Membership in a union of cross products. (Contributed by Mario
Carneiro, 14Feb2015.)



Theorem  raliunxp 4565* 
Write a double restricted quantification as one universal quantifier.
In this version of ralxp 4567, is not assumed to be constant.
(Contributed by Mario Carneiro, 29Dec2014.)



Theorem  rexiunxp 4566* 
Write a double restricted quantification as one universal quantifier.
In this version of rexxp 4568, is not assumed to be constant.
(Contributed by Mario Carneiro, 14Feb2015.)



Theorem  ralxp 4567* 
Universal quantification restricted to a cross product is equivalent to
a double restricted quantification. The hypothesis specifies an
implicit substitution. (Contributed by NM, 7Feb2004.) (Revised by
Mario Carneiro, 29Dec2014.)



Theorem  rexxp 4568* 
Existential quantification restricted to a cross product is equivalent
to a double restricted quantification. (Contributed by NM,
11Nov1995.) (Revised by Mario Carneiro, 14Feb2015.)



Theorem  djussxp 4569* 
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21Nov2014.)



Theorem  ralxpf 4570* 
Version of ralxp 4567 with boundvariable hypotheses. (Contributed
by NM,
18Aug2006.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  rexxpf 4571* 
Version of rexxp 4568 with boundvariable hypotheses. (Contributed
by NM,
19Dec2008.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  iunxpf 4572* 
Indexed union on a cross product is equals a double indexed union. The
hypothesis specifies an implicit substitution. (Contributed by NM,
19Dec2008.)



Theorem  opabbi2dv 4573* 
Deduce equality of a relation and an orderedpair class builder.
Compare abbi2dv 2206. (Contributed by NM, 24Feb2014.)



Theorem  relop 4574* 
A necessary and sufficient condition for a Kuratowski ordered pair to be
a relation. (Contributed by NM, 3Jun2008.) (Avoid depending on this
detail.)



Theorem  ideqg 4575 
For sets, the identity relation is the same as equality. (Contributed
by NM, 30Apr2004.) (Proof shortened by Andrew Salmon,
27Aug2011.)



Theorem  ideq 4576 
For sets, the identity relation is the same as equality. (Contributed
by NM, 13Aug1995.)



Theorem  ididg 4577 
A set is identical to itself. (Contributed by NM, 28May2008.) (Proof
shortened by Andrew Salmon, 27Aug2011.)



Theorem  issetid 4578 
Two ways of expressing set existence. (Contributed by NM, 16Feb2008.)
(Proof shortened by Andrew Salmon, 27Aug2011.) (Revised by Mario
Carneiro, 26Apr2015.)



Theorem  coss1 4579 
Subclass theorem for composition. (Contributed by FL, 30Dec2010.)



Theorem  coss2 4580 
Subclass theorem for composition. (Contributed by NM, 5Apr2013.)



Theorem  coeq1 4581 
Equality theorem for composition of two classes. (Contributed by NM,
3Jan1997.)



Theorem  coeq2 4582 
Equality theorem for composition of two classes. (Contributed by NM,
3Jan1997.)



Theorem  coeq1i 4583 
Equality inference for composition of two classes. (Contributed by NM,
16Nov2000.)



Theorem  coeq2i 4584 
Equality inference for composition of two classes. (Contributed by NM,
16Nov2000.)



Theorem  coeq1d 4585 
Equality deduction for composition of two classes. (Contributed by NM,
16Nov2000.)



Theorem  coeq2d 4586 
Equality deduction for composition of two classes. (Contributed by NM,
16Nov2000.)



Theorem  coeq12i 4587 
Equality inference for composition of two classes. (Contributed by FL,
7Jun2012.)



Theorem  coeq12d 4588 
Equality deduction for composition of two classes. (Contributed by FL,
7Jun2012.)



Theorem  nfco 4589 
Boundvariable hypothesis builder for function value. (Contributed by
NM, 1Sep1999.)



Theorem  elco 4590* 
Elements of a composed relation. (Contributed by BJ, 10Jul2022.)



Theorem  brcog 4591* 
Ordered pair membership in a composition. (Contributed by NM,
24Feb2015.)



Theorem  opelco2g 4592* 
Ordered pair membership in a composition. (Contributed by NM,
27Jan1997.) (Revised by Mario Carneiro, 24Feb2015.)



Theorem  brcogw 4593 
Ordered pair membership in a composition. (Contributed by Thierry
Arnoux, 14Jan2018.)



Theorem  eqbrrdva 4594* 
Deduction from extensionality principle for relations, given an
equivalence only on the relation's domain and range. (Contributed by
Thierry Arnoux, 28Nov2017.)



Theorem  brco 4595* 
Binary relation on a composition. (Contributed by NM, 21Sep2004.)
(Revised by Mario Carneiro, 24Feb2015.)



Theorem  opelco 4596* 
Ordered pair membership in a composition. (Contributed by NM,
27Dec1996.) (Revised by Mario Carneiro, 24Feb2015.)



Theorem  cnvss 4597 
Subset theorem for converse. (Contributed by NM, 22Mar1998.)



Theorem  cnveq 4598 
Equality theorem for converse. (Contributed by NM, 13Aug1995.)



Theorem  cnveqi 4599 
Equality inference for converse. (Contributed by NM, 23Dec2008.)



Theorem  cnveqd 4600 
Equality deduction for converse. (Contributed by NM, 6Dec2013.)

