Type  Label  Description 
Statement 

Theorem  resopab2 5001* 
Restriction of a class abstraction of ordered pairs. (Contributed by
set.mm contributors, 24Aug2007.)



Theorem  dfres2 5002* 
Alternate definition of the restriction operation. (Contributed by
Mario Carneiro, 5Nov2013.)



Theorem  opabresid 5003* 
The restricted identity expressed with the class builder. (Contributed
by FL, 25Apr2012.)



Theorem  dmresi 5004 
The domain of a restricted identity function. (Contributed by set.mm
contributors, 27Aug2004.)



Theorem  resid 5005 
Any class restricted to the universe is itself. (Contributed by set.mm
contributors, 16Mar2004.) (Revised by Scott Fenton, 18Apr2021.)



Theorem  resima 5006 
A restriction to an image. (Contributed by set.mm contributors,
29Sep2004.)



Theorem  resima2 5007 
Image under a restricted class. (Contributed by FL, 31Aug2009.)



Theorem  imadmrn 5008 
The image of the domain of a class is the range of the class.
(Contributed by set.mm contributors, 14Aug1994.)



Theorem  imassrn 5009 
The image of a class is a subset of its range. Theorem 3.16(xi) of
[Monk1] p. 39. (Contributed by set.mm
contributors, 31Mar1995.)



Theorem  imai 5010 
Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38.
(Contributed by set.mm contributors, 30Apr1998.)



Theorem  rnresi 5011 
The range of the restricted identity function. (Contributed by set.mm
contributors, 27Aug2004.)



Theorem  resiima 5012 
The image of a restriction of the identity function. (Contributed by FL,
31Dec2006.)



Theorem  ima0 5013 
Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed
by set.mm contributors, 20May1998.)



Theorem  0ima 5014 
Image under the empty relation. (Contributed by FL, 11Jan2007.)



Theorem  imadisj 5015 
A class whose image under another is empty is disjoint with the other's
domain. (Contributed by FL, 24Jan2007.)



Theorem  cnvimass 5016 
A preimage under any class is included in the domain of the class.
(Contributed by FL, 29Jan2007.)



Theorem  cnvimarndm 5017 
The preimage of the range of a class is the domain of the class.
(Contributed by Jeff Hankins, 15Jul2009.)



Theorem  imasn 5018* 
The image of a singleton. (Contributed by set.mm contributors,
9Jan2015.)



Theorem  elimasn 5019 
Membership in an image of a singleton. (The proof was shortened by
Andrew Salmon, 27Aug2011.) (Contributed by set.mm contributors,
15Mar2004.) (Revised by set.mm contributors, 27Aug2011.)



Theorem  eliniseg 5020 
Membership in an initial segment. The idiom ,
meaning , is used to specify an
initial segment in (for
example) Definition 6.21 of [TakeutiZaring] p. 30. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 28Apr2004.) (Revised by set.mm contributors,
27Aug2011.)



Theorem  epini 5021 
Any set is equal to its preimage under the converse epsilon relation.
(Contributed by Mario Carneiro, 9Mar2013.)



Theorem  iniseg 5022* 
An idiom that signifies an initial segment of an ordering, used, for
example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by
set.mm contributors, 28Apr2004.)



Theorem  imass1 5023 
Subset theorem for image. (Contributed by set.mm contributors,
16Mar2004.)



Theorem  imass2 5024 
Subset theorem for image. Exercise 22(a) of [Enderton] p. 53.
(Contributed by set.mm contributors, 22Mar1998.)



Theorem  ndmima 5025 
The image of a singleton outside the domain is empty. (Contributed by
set.mm contributors, 22May1998.)



Theorem  cotr 5026* 
Two ways of saying a relation is transitive. Definition of transitivity
in [Schechter] p. 51. (The proof was
shortened by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 27Dec1996.)
(Revised by set.mm contributors, 27Aug2011.)



Theorem  cnvsym 5027* 
Two ways of saying a relation is symmetric. Similar to definition of
symmetry in [Schechter] p. 51. (The
proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by set.mm contributors,
28Dec1996.) (Revised by set.mm contributors, 27Aug2011.)



Theorem  intasym 5028* 
Two ways of saying a relation is antisymmetric. Definition of
antisymmetry in [Schechter] p. 51.
(The proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by set.mm contributors, 9Sep2004.)
(Revised by set.mm contributors, 27Aug2011.)



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



Theorem  cnvopab 5030* 
The converse of a class abstraction of ordered pairs. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 11Dec2003.) (Revised by set.mm contributors,
27Aug2011.)



Theorem  cnv0 5031 
The converse of the empty set. (Contributed by set.mm contributors,
6Apr1998.)



Theorem  cnvi 5032 
The converse of the identity relation. Theorem 3.7(ii) of [Monk1]
p. 36. (The proof was shortened by Andrew Salmon, 27Aug2011.)
(Contributed by set.mm contributors, 26Apr1998.) (Revised by set.mm
contributors, 27Aug2011.)



Theorem  cnvun 5033 
The converse of a union is the union of converses. Theorem 16 of
[Suppes] p. 62. (The proof was shortened
by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 25Mar1998.)
(Revised by set.mm contributors, 27Aug2011.)



Theorem  cnvdif 5034 
Distributive law for converse over set difference. (Contributed by
set.mm contributors, 26Jun2014.)



Theorem  cnvin 5035 
Distributive law for converse over intersection. Theorem 15 of [Suppes]
p. 62. (Contributed by set.mm contributors, 25Mar1998.) (Revised by
set.mm contributors, 26Jun2014.)



Theorem  rnun 5036 
Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
(Contributed by set.mm contributors, 24Mar1998.)



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



Theorem  rnuni 5038* 
The range of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by set.mm contributors, 17Mar2004.)



Theorem  imaundi 5039 
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by set.mm contributors, 30Sep2002.)



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



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



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



Theorem  cnvxp 5043 
The converse of a cross product. Exercise 11 of [Suppes] p. 67. (The
proof was shortened by Andrew Salmon, 27Aug2011.) (Contributed by
set.mm contributors, 14Aug1999.) (Revised by set.mm contributors,
27Aug2011.)



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



Theorem  xpnz 5045 
The cross product of nonempty classes is nonempty. (Variation of a
theorem contributed by Raph Levien, 30Jun2006.) (Contributed by
set.mm contributors, 30Jun2006.) (Revised by set.mm contributors,
19Apr2007.)



Theorem  xpeq0 5046 
At least one member of an empty cross product is empty. (Contributed by
set.mm contributors, 27Aug2006.)



Theorem  xpdisj1 5047 
Cross products with disjoint sets are disjoint. (Contributed by set.mm
contributors, 13Sep2004.)



Theorem  xpdisj2 5048 
Cross products with disjoint sets are disjoint. (Contributed by set.mm
contributors, 13Sep2004.)



Theorem  xpsndisj 5049 
Cross products with two different singletons are disjoint. (Contributed
by set.mm contributors, 28Jul2004.) (Revised by set.mm contributors,
3Jun2007.)



Theorem  resdisj 5050 
A double restriction to disjoint classes is the empty set. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 7Oct2004.) (Revised by set.mm contributors,
27Aug2011.)



Theorem  rnxp 5051 
The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37.
(Contributed by set.mm contributors, 12Apr2004.) (Revised by set.mm
contributors, 9Apr2007.)



Theorem  dmxpss 5052 
The domain of a cross product is a subclass of the first factor.
(Contributed by set.mm contributors, 19Mar2007.)



Theorem  rnxpss 5053 
The range of a cross product is a subclass of the second factor. (The
proof was shortened by Andrew Salmon, 27Aug2011.) (Contributed by
set.mm contributors, 16Jan2006.) (Revised by set.mm contributors,
27Aug2011.)



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



Theorem  ssxpb 5055 
A crossproduct subclass relationship is equivalent to the relationship
for it components. (Contributed by set.mm contributors, 17Dec2008.)



Theorem  xp11 5056 
The cross product of nonempty classes is onetoone. (Contributed by
set.mm contributors, 31May2008.)



Theorem  xpcan 5057 
Cancellation law for crossproduct. (Contributed by set.mm contributors,
30Aug2011.)



Theorem  xpcan2 5058 
Cancellation law for crossproduct. (Contributed by set.mm contributors,
30Aug2011.)



Theorem  ssrnres 5059 
Subset of the range of a restriction. (Contributed by set.mm
contributors, 16Jan2006.)



Theorem  rninxp 5060* 
Range of the intersection with a cross product. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 17Jan2006.) (Revised by set.mm contributors,
27Aug2011.)



Theorem  dminxp 5061* 
Domain of the intersection with a cross product. (Contributed by set.mm
contributors, 17Jan2006.)



Theorem  cnvcnv 5062 
The double converse of a class is the original class. (Contributed by
Scott Fenton, 17Apr2021.)



Theorem  cnveqb 5063 
Equality theorem for converse. (Contributed by FL, 19Sep2011.)
(Revised by Scott Fenton, 17Apr2021.)



Theorem  dmsnn0 5064 
The domain of a singleton is nonzero iff the singleton argument is a
set. (Contributed by NM, 14Dec2008.) (Proof shortened by Andrew
Salmon, 27Aug2011.) (Revised by Scott Fenton, 19Apr2021.)



Theorem  rnsnn0 5065 
The range of a singleton is nonzero iff the singleton argument is a set.
(Contributed by set.mm contributors, 14Dec2008.) (Revised by Scott
Fenton, 19Apr2021.)



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



Theorem  dmsnopss 5067 
The domain of a singleton of an ordered pair is a subset of the
singleton of the first member (with no sethood assumptions on ).
(Contributed by Mario Carneiro, 30Apr2015.)



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



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



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



Theorem  op1sta 5072 
Extract the first member of an ordered pair. (Contributed by Raph
Levien, 4Dec2003.)



Theorem  cnvsn 5073 
Converse of a singleton of an ordered pair. (Contributed by NM,
11May1998.)



Theorem  opswap 5074 
Swap the members of an ordered pair. (Contributed by set.mm
contributors, 14Dec2008.)



Theorem  rnsnop 5075 
The range of a singleton of an ordered pair is the singleton of the
second member. (Contributed by set.mm contributors, 24Jul2004.)



Theorem  op2nda 5076 
Extract the second member of an ordered pair. (Contributed by set.mm
contributors, 9Jan2015.)



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



Theorem  resdmres 5078 
Restriction to the domain of a restriction. (Contributed by set.mm
contributors, 8Apr2007.)



Theorem  imadmres 5079 
The image of the domain of a restriction. (Contributed by set.mm
contributors, 8Apr2007.)



Theorem  dfco2 5080* 
Alternate definition of a class composition, using only one bound
variable. (Contributed by set.mm contributors, 19Dec2008.)



Theorem  dfco2a 5081* 
Generalization of dfco2 5080, where can have any value between
and . (The proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by set.mm contributors,
21Dec2008.) (Revised by set.mm contributors, 27Aug2011.)



Theorem  coundi 5082 
Class composition distributes over union. (The proof was shortened by
Andrew Salmon, 27Aug2011.) (Contributed by set.mm contributors,
21Dec2008.) (Revised by set.mm contributors, 27Aug2011.)



Theorem  coundir 5083 
Class composition distributes over union. (The proof was shortened by
Andrew Salmon, 27Aug2011.) (Contributed by set.mm contributors,
21Dec2008.) (Revised by set.mm contributors, 27Aug2011.)



Theorem  cores 5084 
Restricted first member of a class composition. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 12Oct2004.) (Revised by set.mm contributors,
27Aug2011.)



Theorem  resco 5085 
Associative law for the restriction of a composition. (Contributed by
set.mm contributors, 12Dec2006.)



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



Theorem  rnco 5087 
The range of the composition of two classes. (Contributed by set.mm
contributors, 12Dec2006.)



Theorem  rnco2 5088 
The range of the composition of two classes. (Contributed by set.mm
contributors, 27Mar2008.)



Theorem  dmco 5089 
The domain of a composition. Exercise 27 of [Enderton] p. 53.
(Contributed by set.mm contributors, 4Feb2004.)



Theorem  coiun 5090* 
Composition with an indexed union. (Contributed by set.mm contributors,
21Dec2008.)



Theorem  cores2 5091 
Absorption of a reverse (preimage) restriction of the second member of a
class composition. (Contributed by set.mm contributors, 11Dec2006.)



Theorem  co02 5092 
Composition with the empty set. Theorem 20 of [Suppes] p. 63.
(Contributed by set.mm contributors, 24Apr2004.)



Theorem  co01 5093 
Composition with the empty set. (Contributed by set.mm contributors,
24Apr2004.)



Theorem  coi1 5094 
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by set.mm
contributors, 22Apr2004.)
(Revised by Scott Fenton, 14Apr2021.)



Theorem  coi2 5095 
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by set.mm
contributors, 22Apr2004.)
(Revised by Scott Fenton, 17Apr2021.)



Theorem  coires1 5096 
Composition with a restricted identity relation. (Contributed by FL,
19Jun2011.) (Revised by Scott Fenton, 17Apr2021.)



Theorem  coass 5097 
Associative law for class composition. Theorem 27 of [Suppes] p. 64.
Also Exercise 21 of [Enderton] p. 53.
Interestingly, this law holds for
any classes whatsoever, not just functions or even relations.
(Contributed by set.mm contributors, 27Jan1997.)



Theorem  cnvtr 5098 
A class is transitive iff its converse is transitive. (Contributed by FL,
19Sep2011.) (Revised by Scott Fenton, 18Apr2021.)



Theorem  ssdmrn 5099 
A class is included in the cross product of its domain and range.
Exercise 4.12(t) of [Mendelson] p.
235. (Contributed by set.mm
contributors, 3Aug1994.) (Revised by Scott Fenton, 15Apr2021.)



Theorem  dfcnv2 5100 
Definition of converse in terms of image and Swap
. (Contributed by
set.mm contributors, 8Jan2015.)

Swap
