Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  rnxpss 4825 
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 4826 
Upper bound for the domain of a binary relation. (Contributed by BJ,
10Jul2022.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  rnsnop 4874 
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 4875 
Extract the first member of an ordered pair. (See op2nda 4878 to extract
the second member and op1stb 4272 for an alternate version.)
(Contributed
by Raph Levien, 4Dec2003.)



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  mptiniseg 4888* 
Converse singleton image of a function defined by mapsto. (Contributed
by Stefan O'Rear, 25Jan2015.)



Theorem  dmmpt 4889 
The domain of the mapping operation in general. (Contributed by NM,
16May1995.) (Revised by Mario Carneiro, 22Mar2015.)



Theorem  dmmptss 4890* 
The domain of a mapping is a subset of its base class. (Contributed by
Scott Fenton, 17Jun2013.)



Theorem  dmmptg 4891* 
The domain of the mapping operation is the stated domain, if the
function value is always a set. (Contributed by Mario Carneiro,
9Feb2013.) (Revised by Mario Carneiro, 14Sep2013.)



Theorem  relco 4892 
A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25.
(Contributed by NM, 26Jan1997.)



Theorem  dfco2 4893* 
Alternate definition of a class composition, using only one bound
variable. (Contributed by NM, 19Dec2008.)



Theorem  dfco2a 4894* 
Generalization of dfco2 4893, where can have any value between
and .
(Contributed by NM, 21Dec2008.)
(Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  coundi 4895 
Class composition distributes over union. (Contributed by NM,
21Dec2008.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  coundir 4896 
Class composition distributes over union. (Contributed by NM,
21Dec2008.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  cores 4897 
Restricted first member of a class composition. (Contributed by NM,
12Oct2004.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  resco 4898 
Associative law for the restriction of a composition. (Contributed by
NM, 12Dec2006.)



Theorem  imaco 4899 
Image of the composition of two classes. (Contributed by Jason
Orendorff, 12Dec2006.)



Theorem  rnco 4900 
The range of the composition of two classes. (Contributed by NM,
12Dec2006.)

