Type  Label  Description 
Statement 

Theorem  imass2 4701 
Subset theorem for image. Exercise 22(a) of [Enderton] p. 53.
(Contributed by NM, 22Mar1998.)



Theorem  ndmima 4702 
The image of a singleton outside the domain is empty. (Contributed by NM,
22May1998.)



Theorem  relcnv 4703 
A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed
by NM, 29Oct1996.)



Theorem  relbrcnvg 4704 
When is a relation,
the sethood assumptions on brcnv 4518 can be
omitted. (Contributed by Mario Carneiro, 28Apr2015.)



Theorem  relbrcnv 4705 
When is a relation,
the sethood assumptions on brcnv 4518 can be
omitted. (Contributed by Mario Carneiro, 28Apr2015.)



Theorem  cotr 4706* 
Two ways of saying a relation is transitive. Definition of transitivity
in [Schechter] p. 51. (Contributed by
NM, 27Dec1996.) (Proof
shortened by Andrew Salmon, 27Aug2011.)



Theorem  issref 4707* 
Two ways to state a relation is reflexive. Adapted from Tarski.
(Contributed by FL, 15Jan2012.) (Revised by NM, 30Mar2016.)



Theorem  cnvsym 4708* 
Two ways of saying a relation is symmetric. Similar to definition of
symmetry in [Schechter] p. 51.
(Contributed by NM, 28Dec1996.)
(Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  intasym 4709* 
Two ways of saying a relation is antisymmetric. Definition of
antisymmetry in [Schechter] p. 51.
(Contributed by NM, 9Sep2004.)
(Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  asymref 4710* 
Two ways of saying a relation is antisymmetric and reflexive.
is the field of a relation by relfld 4846. (Contributed by
NM, 6May2008.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  intirr 4711* 
Two ways of saying a relation is irreflexive. Definition of
irreflexivity in [Schechter] p. 51.
(Contributed by NM, 9Sep2004.)
(Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  brcodir 4712* 
Two ways of saying that two elements have an upper bound. (Contributed
by Mario Carneiro, 3Nov2015.)



Theorem  codir 4713* 
Two ways of saying a relation is directed. (Contributed by Mario
Carneiro, 22Nov2013.)



Theorem  qfto 4714* 
A quantifierfree way of expressing the total order predicate.
(Contributed by Mario Carneiro, 22Nov2013.)



Theorem  xpidtr 4715 
A square cross product is a transitive relation.
(Contributed by FL, 31Jul2009.)



Theorem  trin2 4716 
The intersection of two transitive classes is transitive. (Contributed
by FL, 31Jul2009.)



Theorem  poirr2 4717 
A partial order relation is irreflexive. (Contributed by Mario
Carneiro, 2Nov2015.)



Theorem  trinxp 4718 
The relation induced by a transitive relation on a part of its field is
transitive. (Taking the intersection of a relation with a square cross
product is a way to restrict it to a subset of its field.) (Contributed
by FL, 31Jul2009.)



Theorem  soirri 4719 
A strict order relation is irreflexive. (Contributed by NM,
10Feb1996.) (Revised by Mario Carneiro, 10May2013.)



Theorem  sotri 4720 
A strict order relation is a transitive relation. (Contributed by NM,
10Feb1996.) (Revised by Mario Carneiro, 10May2013.)



Theorem  son2lpi 4721 
A strict order relation has no 2cycle loops. (Contributed by NM,
10Feb1996.) (Revised by Mario Carneiro, 10May2013.)



Theorem  sotri2 4722 
A transitivity relation. (Read B < A and B < C implies A <
C .) (Contributed by Mario Carneiro, 10May2013.)



Theorem  sotri3 4723 
A transitivity relation. (Read A < B and C < B implies A <
C .) (Contributed by Mario Carneiro, 10May2013.)



Theorem  poleloe 4724 
Express "less than or equals" for general strict orders.
(Contributed by
Stefan O'Rear, 17Jan2015.)



Theorem  poltletr 4725 
Transitive law for general strict orders. (Contributed by Stefan O'Rear,
17Jan2015.)



Theorem  cnvopab 4726* 
The converse of a class abstraction of ordered pairs. (Contributed by
NM, 11Dec2003.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  cnv0 4727 
The converse of the empty set. (Contributed by NM, 6Apr1998.)



Theorem  cnvi 4728 
The converse of the identity relation. Theorem 3.7(ii) of [Monk1]
p. 36. (Contributed by NM, 26Apr1998.) (Proof shortened by Andrew
Salmon, 27Aug2011.)



Theorem  cnvun 4729 
The converse of a union is the union of converses. Theorem 16 of
[Suppes] p. 62. (Contributed by NM,
25Mar1998.) (Proof shortened by
Andrew Salmon, 27Aug2011.)



Theorem  cnvdif 4730 
Distributive law for converse over set difference. (Contributed by
Mario Carneiro, 26Jun2014.)



Theorem  cnvin 4731 
Distributive law for converse over intersection. Theorem 15 of [Suppes]
p. 62. (Contributed by NM, 25Mar1998.) (Revised by Mario Carneiro,
26Jun2014.)



Theorem  rnun 4732 
Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
(Contributed by NM, 24Mar1998.)



Theorem  rnin 4733 
The range of an intersection belongs the intersection of ranges. Theorem
9 of [Suppes] p. 60. (Contributed by NM,
15Sep2004.)



Theorem  rniun 4734 
The range of an indexed union. (Contributed by Mario Carneiro,
29May2015.)



Theorem  rnuni 4735* 
The range of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by NM, 17Mar2004.) (Revised by Mario Carneiro,
29May2015.)



Theorem  imaundi 4736 
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by NM, 30Sep2002.)



Theorem  imaundir 4737 
The image of a union. (Contributed by Jeff Hoffman, 17Feb2008.)



Theorem  dminss 4738 
An upper bound for intersection with a domain. Theorem 40 of [Suppes]
p. 66, who calls it "somewhat surprising." (Contributed by
NM,
11Aug2004.)



Theorem  imainss 4739 
An upper bound for intersection with an image. Theorem 41 of [Suppes]
p. 66. (Contributed by NM, 11Aug2004.)



Theorem  inimass 4740 
The image of an intersection (Contributed by Thierry Arnoux,
16Dec2017.)



Theorem  inimasn 4741 
The intersection of the image of singleton (Contributed by Thierry
Arnoux, 16Dec2017.)



Theorem  cnvxp 4742 
The converse of a cross product. Exercise 11 of [Suppes] p. 67.
(Contributed by NM, 14Aug1999.) (Proof shortened by Andrew Salmon,
27Aug2011.)



Theorem  xp0 4743 
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
12Apr2004.)



Theorem  xpmlem 4744* 
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 11Dec2018.)



Theorem  xpm 4745* 
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 13Dec2018.)



Theorem  xpeq0r 4746 
A cross product is empty if at least one member is empty. (Contributed by
Jim Kingdon, 12Dec2018.)



Theorem  xpdisj1 4747 
Cross products with disjoint sets are disjoint. (Contributed by NM,
13Sep2004.)



Theorem  xpdisj2 4748 
Cross products with disjoint sets are disjoint. (Contributed by NM,
13Sep2004.)



Theorem  xpsndisj 4749 
Cross products with two different singletons are disjoint. (Contributed
by NM, 28Jul2004.)



Theorem  djudisj 4750* 
Disjoint unions with disjoint index sets are disjoint. (Contributed by
Stefan O'Rear, 21Nov2014.)



Theorem  resdisj 4751 
A double restriction to disjoint classes is the empty set. (Contributed
by NM, 7Oct2004.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  rnxpm 4752* 
The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37,
with nonempty changed to inhabited. (Contributed by Jim Kingdon,
12Dec2018.)



Theorem  dmxpss 4753 
The domain of a cross product is a subclass of the first factor.
(Contributed by NM, 19Mar2007.)



Theorem  rnxpss 4754 
The range of a cross product is a subclass of the second factor.
(Contributed by NM, 16Jan2006.) (Proof shortened by Andrew Salmon,
27Aug2011.)



Theorem  rnxpid 4755 
The range of a square cross product. (Contributed by FL,
17May2010.)



Theorem  ssxpbm 4756* 
A crossproduct subclass relationship is equivalent to the relationship
for its components. (Contributed by Jim Kingdon, 12Dec2018.)



Theorem  ssxp1 4757* 
Cross product subset cancellation. (Contributed by Jim Kingdon,
14Dec2018.)



Theorem  ssxp2 4758* 
Cross product subset cancellation. (Contributed by Jim Kingdon,
14Dec2018.)



Theorem  xp11m 4759* 
The cross product of inhabited classes is onetoone. (Contributed by
Jim Kingdon, 13Dec2018.)



Theorem  xpcanm 4760* 
Cancellation law for crossproduct. (Contributed by Jim Kingdon,
14Dec2018.)



Theorem  xpcan2m 4761* 
Cancellation law for crossproduct. (Contributed by Jim Kingdon,
14Dec2018.)



Theorem  xpexr2m 4762* 
If a nonempty cross product is a set, so are both of its components.
(Contributed by Jim Kingdon, 14Dec2018.)



Theorem  ssrnres 4763 
Subset of the range of a restriction. (Contributed by NM,
16Jan2006.)



Theorem  rninxp 4764* 
Range of the intersection with a cross product. (Contributed by NM,
17Jan2006.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  dminxp 4765* 
Domain of the intersection with a cross product. (Contributed by NM,
17Jan2006.)



Theorem  imainrect 4766 
Image of a relation restricted to a rectangular region. (Contributed by
Stefan O'Rear, 19Feb2015.)



Theorem  xpima1 4767 
The image by a cross product. (Contributed by Thierry Arnoux,
16Dec2017.)



Theorem  xpima2m 4768* 
The image by a cross product. (Contributed by Thierry Arnoux,
16Dec2017.)



Theorem  xpimasn 4769 
The image of a singleton by a cross product. (Contributed by Thierry
Arnoux, 14Jan2018.)



Theorem  cnvcnv3 4770* 
The set of all ordered pairs in a class is the same as the double
converse. (Contributed by Mario Carneiro, 16Aug2015.)



Theorem  dfrel2 4771 
Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25.
(Contributed by NM, 29Dec1996.)



Theorem  dfrel4v 4772* 
A relation can be expressed as the set of ordered pairs in it.
(Contributed by Mario Carneiro, 16Aug2015.)



Theorem  cnvcnv 4773 
The double converse of a class strips out all elements that are not
ordered pairs. (Contributed by NM, 8Dec2003.)



Theorem  cnvcnv2 4774 
The double converse of a class equals its restriction to the universe.
(Contributed by NM, 8Oct2007.)



Theorem  cnvcnvss 4775 
The double converse of a class is a subclass. Exercise 2 of
[TakeutiZaring] p. 25. (Contributed
by NM, 23Jul2004.)



Theorem  cnveqb 4776 
Equality theorem for converse. (Contributed by FL, 19Sep2011.)



Theorem  cnveq0 4777 
A relation empty iff its converse is empty. (Contributed by FL,
19Sep2011.)



Theorem  dfrel3 4778 
Alternate definition of relation. (Contributed by NM, 14May2008.)



Theorem  dmresv 4779 
The domain of a universal restriction. (Contributed by NM,
14May2008.)



Theorem  rnresv 4780 
The range of a universal restriction. (Contributed by NM,
14May2008.)



Theorem  dfrn4 4781 
Range defined in terms of image. (Contributed by NM, 14May2008.)



Theorem  csbrng 4782 
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10Nov2012.)



Theorem  rescnvcnv 4783 
The restriction of the double converse of a class. (Contributed by NM,
8Apr2007.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  cnvcnvres 4784 
The double converse of the restriction of a class. (Contributed by NM,
3Jun2007.)



Theorem  imacnvcnv 4785 
The image of the double converse of a class. (Contributed by NM,
8Apr2007.)



Theorem  dmsnm 4786* 
The domain of a singleton is inhabited iff the singleton argument is an
ordered pair. (Contributed by Jim Kingdon, 15Dec2018.)



Theorem  rnsnm 4787* 
The range of a singleton is inhabited iff the singleton argument is an
ordered pair. (Contributed by Jim Kingdon, 15Dec2018.)



Theorem  dmsn0 4788 
The domain of the singleton of the empty set is empty. (Contributed by
NM, 30Jan2004.)



Theorem  cnvsn0 4789 
The converse of the singleton of the empty set is empty. (Contributed by
Mario Carneiro, 30Aug2015.)



Theorem  dmsn0el 4790 
The domain of a singleton is empty if the singleton's argument contains
the empty set. (Contributed by NM, 15Dec2008.)



Theorem  relsn2m 4791* 
A singleton is a relation iff it has an inhabited domain. (Contributed
by Jim Kingdon, 16Dec2018.)



Theorem  dmsnopg 4792 
The domain of a singleton of an ordered pair is the singleton of the
first member. (Contributed by Mario Carneiro, 26Apr2015.)



Theorem  dmpropg 4793 
The domain of an unordered pair of ordered pairs. (Contributed by Mario
Carneiro, 26Apr2015.)



Theorem  dmsnop 4794 
The domain of a singleton of an ordered pair is the singleton of the
first member. (Contributed by NM, 30Jan2004.) (Proof shortened by
Andrew Salmon, 27Aug2011.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  dmprop 4795 
The domain of an unordered pair of ordered pairs. (Contributed by NM,
13Sep2011.)



Theorem  dmtpop 4796 
The domain of an unordered triple of ordered pairs. (Contributed by NM,
14Sep2011.)



Theorem  cnvcnvsn 4797 
Double converse of a singleton of an ordered pair. (Unlike cnvsn 4803,
this does not need any sethood assumptions on and .)
(Contributed by Mario Carneiro, 26Apr2015.)



Theorem  dmsnsnsng 4798 
The domain of the singleton of the singleton of a singleton.
(Contributed by Jim Kingdon, 16Dec2018.)



Theorem  rnsnopg 4799 
The range of a singleton of an ordered pair is the singleton of the second
member. (Contributed by NM, 24Jul2004.) (Revised by Mario Carneiro,
30Apr2015.)



Theorem  rnpropg 4800 
The range of a pair of ordered pairs is the pair of second members.
(Contributed by Thierry Arnoux, 3Jan2017.)

