Type  Label  Description 
Statement 

Theorem  xpeq12i 4601 
Equality inference for cross product. (Contributed by FL,
31Aug2009.)



Theorem  xpeq1d 4602 
Equality deduction for cross product. (Contributed by Jeff Madsen,
17Jun2010.)



Theorem  xpeq2d 4603 
Equality deduction for cross product. (Contributed by Jeff Madsen,
17Jun2010.)



Theorem  xpeq12d 4604 
Equality deduction for Cartesian product. (Contributed by NM,
8Dec2013.)



Theorem  sqxpeqd 4605 
Equality deduction for a Cartesian square, see Wikipedia "Cartesian
product",
https://en.wikipedia.org/wiki/Cartesian_product#nary_Cartesian_power.
(Contributed by AV, 13Jan2020.)



Theorem  nfxp 4606 
Boundvariable hypothesis builder for cross product. (Contributed by
NM, 15Sep2003.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  0nelxp 4607 
The empty set is not a member of a cross product. (Contributed by NM,
2May1996.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  0nelelxp 4608 
A member of a cross product (ordered pair) doesn't contain the empty
set. (Contributed by NM, 15Dec2008.)



Theorem  opelxp 4609 
Ordered pair membership in a cross product. (Contributed by NM,
15Nov1994.) (Proof shortened by Andrew Salmon, 12Aug2011.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  brxp 4610 
Binary relation on a cross product. (Contributed by NM,
22Apr2004.)



Theorem  opelxpi 4611 
Ordered pair membership in a cross product (implication). (Contributed by
NM, 28May1995.)



Theorem  opelxpd 4612 
Ordered pair membership in a Cartesian product, deduction form.
(Contributed by Glauco Siliprandi, 3Mar2021.)



Theorem  opelxp1 4613 
The first member of an ordered pair of classes in a cross product belongs
to first cross product argument. (Contributed by NM, 28May2008.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  opelxp2 4614 
The second member of an ordered pair of classes in a cross product belongs
to second cross product argument. (Contributed by Mario Carneiro,
26Apr2015.)



Theorem  otelxp1 4615 
The first member of an ordered triple of classes in a cross product
belongs to first cross product argument. (Contributed by NM,
28May2008.)



Theorem  rabxp 4616* 
Membership in a class builder restricted to a cross product.
(Contributed by NM, 20Feb2014.)



Theorem  brrelex12 4617 
A true binary relation on a relation implies the arguments are sets.
(This is a property of our ordered pair definition.) (Contributed by
Mario Carneiro, 26Apr2015.)



Theorem  brrelex1 4618 
A true binary relation on a relation implies the first argument is a set.
(This is a property of our ordered pair definition.) (Contributed by NM,
18May2004.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  brrelex 4619 
A true binary relation on a relation implies the first argument is a set.
(This is a property of our ordered pair definition.) (Contributed by NM,
18May2004.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  brrelex2 4620 
A true binary relation on a relation implies the second argument is a set.
(This is a property of our ordered pair definition.) (Contributed by
Mario Carneiro, 26Apr2015.)



Theorem  brrelex12i 4621 
Two classes that are related by a binary relation are sets. (An
artifact of our ordered pair definition.) (Contributed by BJ,
3Oct2022.)



Theorem  brrelex1i 4622 
The first argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by NM, 4Jun1998.)



Theorem  brrelex2i 4623 
The second argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by Mario Carneiro,
26Apr2015.)



Theorem  nprrel 4624 
No proper class is related to anything via any relation. (Contributed
by Roy F. Longton, 30Jul2005.)



Theorem  0nelrel 4625 
A binary relation does not contain the empty set. (Contributed by AV,
15Nov2021.)



Theorem  fconstmpt 4626* 
Representation of a constant function using the mapping operation.
(Note that
cannot appear free in .) (Contributed by NM,
12Oct1999.) (Revised by Mario Carneiro, 16Nov2013.)



Theorem  vtoclr 4627* 
Variable to class conversion of transitive relation. (Contributed by
NM, 9Jun1998.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  opelvvg 4628 
Ordered pair membership in the universal class of ordered pairs.
(Contributed by Mario Carneiro, 3May2015.)



Theorem  opelvv 4629 
Ordered pair membership in the universal class of ordered pairs.
(Contributed by NM, 22Aug2013.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  opthprc 4630 
Justification theorem for an ordered pair definition that works for any
classes, including proper classes. This is a possible definition
implied by the footnote in [Jech] p. 78,
which says, "The sophisticated
reader will not object to our use of a pair of classes."
(Contributed
by NM, 28Sep2003.)



Theorem  brel 4631 
Two things in a binary relation belong to the relation's domain.
(Contributed by NM, 17May1996.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  brab2a 4632* 
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 9Nov2015.)



Theorem  elxp3 4633* 
Membership in a cross product. (Contributed by NM, 5Mar1995.)



Theorem  opeliunxp 4634 
Membership in a union of cross products. (Contributed by Mario
Carneiro, 29Dec2014.) (Revised by Mario Carneiro, 1Jan2017.)



Theorem  xpundi 4635 
Distributive law for cross product over union. Theorem 103 of [Suppes]
p. 52. (Contributed by NM, 12Aug2004.)



Theorem  xpundir 4636 
Distributive law for cross product over union. Similar to Theorem 103
of [Suppes] p. 52. (Contributed by NM,
30Sep2002.)



Theorem  xpiundi 4637* 
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27Apr2014.)



Theorem  xpiundir 4638* 
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27Apr2014.)



Theorem  iunxpconst 4639* 
Membership in a union of cross products when the second factor is
constant. (Contributed by Mario Carneiro, 29Dec2014.)



Theorem  xpun 4640 
The cross product of two unions. (Contributed by NM, 12Aug2004.)



Theorem  elvv 4641* 
Membership in universal class of ordered pairs. (Contributed by NM,
4Jul1994.)



Theorem  elvvv 4642* 
Membership in universal class of ordered triples. (Contributed by NM,
17Dec2008.)



Theorem  elvvuni 4643 
An ordered pair contains its union. (Contributed by NM,
16Sep2006.)



Theorem  mosubopt 4644* 
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28Aug2007.)



Theorem  mosubop 4645* 
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28May1995.)



Theorem  brinxp2 4646 
Intersection of binary relation with Cartesian product. (Contributed by
NM, 3Mar2007.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  brinxp 4647 
Intersection of binary relation with Cartesian product. (Contributed by
NM, 9Mar1997.)



Theorem  poinxp 4648 
Intersection of partial order with cross product of its field.
(Contributed by Mario Carneiro, 10Jul2014.)



Theorem  soinxp 4649 
Intersection of linear order with cross product of its field.
(Contributed by Mario Carneiro, 10Jul2014.)



Theorem  seinxp 4650 
Intersection of setlike relation with cross product of its field.
(Contributed by Mario Carneiro, 22Jun2015.)

Se
Se 

Theorem  posng 4651 
Partial ordering of a singleton. (Contributed by Jim Kingdon,
5Dec2018.)



Theorem  sosng 4652 
Strict linear ordering on a singleton. (Contributed by Jim Kingdon,
5Dec2018.)



Theorem  opabssxp 4653* 
An abstraction relation is a subset of a related cross product.
(Contributed by NM, 16Jul1995.)



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



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



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



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



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



Theorem  0xp 4659 
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 4660 
Distribute proper substitution through the cross product of two classes.
(Contributed by Alan Sare, 10Nov2012.)



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



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



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



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



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



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



Theorem  ssrel 4667* 
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 4668* 
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2Aug1994.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  xpss12 4686 
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 4687 
A cross product is included in the ordered pair universe. Exercise 3 of
[TakeutiZaring] p. 25. (Contributed
by NM, 2Aug1994.)



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



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



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



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



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



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



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



Theorem  sqxpexg 4695 
The Cartesian square of a set is a set. (Contributed by AV,
13Jan2020.)



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



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



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



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



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

