Type  Label  Description 
Statement 

Theorem  iss 4801 
A subclass of the identity function is the identity function restricted
to its domain. (Contributed by NM, 13Dec2003.) (Proof shortened by
Andrew Salmon, 27Aug2011.)



Theorem  resopab2 4802* 
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 24Aug2007.)



Theorem  resmpt 4803* 
Restriction of the mapping operation. (Contributed by Mario Carneiro,
15Jul2013.)



Theorem  resmpt3 4804* 
Unconditional restriction of the mapping operation. (Contributed by
Stefan O'Rear, 24Jan2015.) (Proof shortened by Mario Carneiro,
22Mar2015.)



Theorem  resmptf 4805 
Restriction of the mapping operation. (Contributed by Thierry Arnoux,
28Mar2017.)



Theorem  resmptd 4806* 
Restriction of the mapping operation, deduction form. (Contributed by
Glauco Siliprandi, 11Dec2019.)



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



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



Theorem  mptresid 4809* 
The restricted identity expressed with the mapsto notation.
(Contributed by FL, 25Apr2012.)



Theorem  dmresi 4810 
The domain of a restricted identity function. (Contributed by NM,
27Aug2004.)



Theorem  resid 4811 
Any relation restricted to the universe is itself. (Contributed by NM,
16Mar2004.)



Theorem  imaeq1 4812 
Equality theorem for image. (Contributed by NM, 14Aug1994.)



Theorem  imaeq2 4813 
Equality theorem for image. (Contributed by NM, 14Aug1994.)



Theorem  imaeq1i 4814 
Equality theorem for image. (Contributed by NM, 21Dec2008.)



Theorem  imaeq2i 4815 
Equality theorem for image. (Contributed by NM, 21Dec2008.)



Theorem  imaeq1d 4816 
Equality theorem for image. (Contributed by FL, 15Dec2006.)



Theorem  imaeq2d 4817 
Equality theorem for image. (Contributed by FL, 15Dec2006.)



Theorem  imaeq12d 4818 
Equality theorem for image. (Contributed by Mario Carneiro,
4Dec2016.)



Theorem  dfima2 4819* 
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 19Apr2004.) (Proof shortened by Andrew
Salmon, 27Aug2011.)



Theorem  dfima3 4820* 
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 14Aug1994.) (Proof shortened by Andrew
Salmon, 27Aug2011.)



Theorem  elimag 4821* 
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 20Jan2007.)



Theorem  elima 4822* 
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 19Apr2004.)



Theorem  elima2 4823* 
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 11Aug2004.)



Theorem  elima3 4824* 
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 14Aug1994.)



Theorem  nfima 4825 
Boundvariable hypothesis builder for image. (Contributed by NM,
30Dec1996.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  nfimad 4826 
Deduction version of boundvariable hypothesis builder nfima 4825.
(Contributed by FL, 15Dec2006.) (Revised by Mario Carneiro,
15Oct2016.)



Theorem  imadmrn 4827 
The image of the domain of a class is the range of the class.
(Contributed by NM, 14Aug1994.)



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



Theorem  imaexg 4829 
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed
by NM, 24Jul1995.)



Theorem  imaex 4830 
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39.
(Contributed by JJ, 24Sep2021.)



Theorem  imai 4831 
Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38.
(Contributed by NM, 30Apr1998.)



Theorem  rnresi 4832 
The range of the restricted identity function. (Contributed by NM,
27Aug2004.)



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



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



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



Theorem  csbima12g 4836 
Move class substitution in and out of the image of a function.
(Contributed by FL, 15Dec2006.) (Proof shortened by Mario Carneiro,
4Dec2016.)



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



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



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



Theorem  imasng 4840* 
The image of a singleton. (Contributed by NM, 8May2005.)



Theorem  elreimasng 4841 
Elementhood in the image of a singleton. (Contributed by Jim Kingdon,
10Dec2018.)



Theorem  elimasn 4842 
Membership in an image of a singleton. (Contributed by NM,
15Mar2004.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  elimasng 4843 
Membership in an image of a singleton. (Contributed by Raph Levien,
21Oct2006.)



Theorem  args 4844* 
Two ways to express the class of uniquevalued arguments of ,
which is the same as the domain of whenever is a function.
The lefthand side of the equality is from Definition 10.2 of [Quine]
p. 65. Quine uses the notation "arg " for this class (for which
we have no separate notation). (Contributed by NM, 8May2005.)



Theorem  eliniseg 4845 
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. (Contributed by
NM, 28Apr2004.) (Proof shortened by Andrew Salmon, 27Aug2011.)



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



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



Theorem  dfse2 4848* 
Alternate definition of setlike relation. (Contributed by Mario
Carneiro, 23Jun2015.)

Se


Theorem  exse2 4849 
Any set relation is setlike. (Contributed by Mario Carneiro,
22Jun2015.)

Se 

Theorem  imass1 4850 
Subset theorem for image. (Contributed by NM, 16Mar2004.)



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



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



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



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



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



Theorem  cotr 4856* 
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 4857* 
Two ways to state a relation is reflexive. Adapted from Tarski.
(Contributed by FL, 15Jan2012.) (Revised by NM, 30Mar2016.)



Theorem  cnvsym 4858* 
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 4859* 
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 4860* 
Two ways of saying a relation is antisymmetric and reflexive.
is the field of a relation by relfld 5003. (Contributed by
NM, 6May2008.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  intirr 4861* 
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 4862* 
Two ways of saying that two elements have an upper bound. (Contributed
by Mario Carneiro, 3Nov2015.)



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



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



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



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



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



Theorem  trinxp 4868 
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 4869 
A strict order relation is irreflexive. (Contributed by NM,
10Feb1996.) (Revised by Mario Carneiro, 10May2013.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

