Type  Label  Description 
Statement 

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



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



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



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



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



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



Theorem  imassrn 4707 
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 4708 
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed
by NM, 24Jul1995.)



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  args 4722* 
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 4723 
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 4724 
Any set is equal to its preimage under the converse epsilon relation.
(Contributed by Mario Carneiro, 9Mar2013.)



Theorem  iniseg 4725* 
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 4726* 
Alternate definition of setlike relation. (Contributed by Mario
Carneiro, 23Jun2015.)

Se


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

Se 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  rnxpss 4782 
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 4783 
The range of a square cross product. (Contributed by FL,
17May2010.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

