Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



Theorem  mptcnv 4909* 
The converse of a mapping function. (Contributed by Thierry Arnoux,
16Jan2017.)



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



Theorem  cnvi 4911 
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 4912 
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 4913 
Distributive law for converse over set difference. (Contributed by
Mario Carneiro, 26Jun2014.)



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



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



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



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



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



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



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



Theorem  dminss 4921 
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 4922 
An upper bound for intersection with an image. Theorem 41 of [Suppes]
p. 66. (Contributed by NM, 11Aug2004.)



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



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



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



Theorem  xp0 4926 
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 4927* 
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 11Dec2018.)



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



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



Theorem  sqxpeq0 4930 
A Cartesian square is empty iff its member is empty. (Contributed by Jim
Kingdon, 21Apr2023.)



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



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



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



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



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



Theorem  rnxpm 4936* 
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 4937 
The domain of a cross product is a subclass of the first factor.
(Contributed by NM, 19Mar2007.)



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



Theorem  dmxpss2 4939 
Upper bound for the domain of a binary relation. (Contributed by BJ,
10Jul2022.)



Theorem  rnxpss2 4940 
Upper bound for the range of a binary relation. (Contributed by BJ,
10Jul2022.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dmsnop 4980 
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 4981 
The domain of an unordered pair of ordered pairs. (Contributed by NM,
13Sep2011.)



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



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



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



Theorem  rnsnopg 4985 
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 4986 
The range of a pair of ordered pairs is the pair of second members.
(Contributed by Thierry Arnoux, 3Jan2017.)



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



Theorem  op1sta 4988 
Extract the first member of an ordered pair. (See op2nda 4991 to extract
the second member and op1stb 4367 for an alternate version.)
(Contributed
by Raph Levien, 4Dec2003.)



Theorem  cnvsn 4989 
Converse of a singleton of an ordered pair. (Contributed by NM,
11May1998.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  op2ndb 4990 
Extract the second member of an ordered pair. Theorem 5.12(ii) of
[Monk1] p. 52. (See op1stb 4367 to extract the first member and op2nda 4991
for an alternate version.) (Contributed by NM, 25Nov2003.)



Theorem  op2nda 4991 
Extract the second member of an ordered pair. (See op1sta 4988 to extract
the first member and op2ndb 4990 for an alternate version.) (Contributed
by NM, 17Feb2004.) (Proof shortened by Andrew Salmon,
27Aug2011.)



Theorem  cnvsng 4992 
Converse of a singleton of an ordered pair. (Contributed by NM,
23Jan2015.)



Theorem  opswapg 4993 
Swap the members of an ordered pair. (Contributed by Jim Kingdon,
16Dec2018.)



Theorem  elxp4 4994 
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp5 4995. (Contributed by NM,
17Feb2004.)



Theorem  elxp5 4995 
Membership in a cross product requiring no quantifiers or dummy
variables. Provides a slightly shorter version of elxp4 4994 when the
double intersection does not create class existence problems (caused by
int0 3753). (Contributed by NM, 1Aug2004.)



Theorem  cnvresima 4996 
An image under the converse of a restriction. (Contributed by Jeff
Hankins, 12Jul2009.)



Theorem  resdm2 4997 
A class restricted to its domain equals its double converse. (Contributed
by NM, 8Apr2007.)



Theorem  resdmres 4998 
Restriction to the domain of a restriction. (Contributed by NM,
8Apr2007.)



Theorem  imadmres 4999 
The image of the domain of a restriction. (Contributed by NM,
8Apr2007.)



Theorem  mptpreima 5000* 
The preimage of a function in mapsto notation. (Contributed by Stefan
O'Rear, 25Jan2015.)

