Type  Label  Description 
Statement 

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



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



Theorem  mptresid 4603* 
The restricted identity expressed with the "maps to" notation.
(Contributed by FL, 25Apr2012.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

Se 

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

Se 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

