Type  Label  Description 
Statement 

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



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



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



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



Theorem  opelxp1 4405 
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 4406 
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 4407 
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 4408* 
Membership in a class builder restricted to a cross product.
(Contributed by NM, 20Feb2014.)



Theorem  brrelex12 4409 
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  brrelex 4410 
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 4411 
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  brrelexi 4412 
The first argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by NM, 4Jun1998.)



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



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



Theorem  fconstmpt 4415* 
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 4416* 
Variable to class conversion of transitive relation. (Contributed by
NM, 9Jun1998.) (Revised by Mario Carneiro, 26Apr2015.)



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



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



Theorem  opthprc 4419 
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 4420 
Two things in a binary relation belong to the relation's domain.
(Contributed by NM, 17May1996.) (Revised by Mario Carneiro,
26Apr2015.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

Se
Se 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  reliin 4487 
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 4488* 
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 4489* 
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8Mar2014.)



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



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



Theorem  relopab 4492 
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 4493 
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 4494 
The membership relation is a relation. (Contributed by NM,
26Apr1998.) (Revised by Mario Carneiro, 21Dec2013.)



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



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



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



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



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



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

