Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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

Se
Se 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ralxp 4479* 
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 4480* 
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 4481* 
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21Nov2014.)



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



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



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



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



Theorem  relop 4486* 
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 4487 
For sets, the identity relation is the same as equality. (Contributed
by NM, 30Apr2004.) (Proof shortened by Andrew Salmon,
27Aug2011.)



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



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



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



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



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



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



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



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



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



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



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



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



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

