Type  Label  Description 
Statement 

Theorem  dmcoss 4601 
Domain of a composition. Theorem 21 of [Suppes]
p. 63. (Contributed by
NM, 19Mar1998.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  rncoss 4602 
Range of a composition. (Contributed by NM, 19Mar1998.)



Theorem  dmcosseq 4603 
Domain of a composition. (Contributed by NM, 28May1998.) (Proof
shortened by Andrew Salmon, 27Aug2011.)



Theorem  dmcoeq 4604 
Domain of a composition. (Contributed by NM, 19Mar1998.)



Theorem  rncoeq 4605 
Range of a composition. (Contributed by NM, 19Mar1998.)



Theorem  reseq1 4606 
Equality theorem for restrictions. (Contributed by NM, 7Aug1994.)



Theorem  reseq2 4607 
Equality theorem for restrictions. (Contributed by NM, 8Aug1994.)



Theorem  reseq1i 4608 
Equality inference for restrictions. (Contributed by NM,
21Oct2014.)



Theorem  reseq2i 4609 
Equality inference for restrictions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  reseq12i 4610 
Equality inference for restrictions. (Contributed by NM,
21Oct2014.)



Theorem  reseq1d 4611 
Equality deduction for restrictions. (Contributed by NM,
21Oct2014.)



Theorem  reseq2d 4612 
Equality deduction for restrictions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  reseq12d 4613 
Equality deduction for restrictions. (Contributed by NM,
21Oct2014.)



Theorem  nfres 4614 
Boundvariable hypothesis builder for restriction. (Contributed by NM,
15Sep2003.) (Revised by David Abernethy, 19Jun2012.)



Theorem  csbresg 4615 
Distribute proper substitution through the restriction of a class.
(Contributed by Alan Sare, 10Nov2012.)



Theorem  res0 4616 
A restriction to the empty set is empty. (Contributed by NM,
12Nov1994.)



Theorem  opelres 4617 
Ordered pair membership in a restriction. Exercise 13 of
[TakeutiZaring] p. 25.
(Contributed by NM, 13Nov1995.)



Theorem  brres 4618 
Binary relation on a restriction. (Contributed by NM, 12Dec2006.)



Theorem  opelresg 4619 
Ordered pair membership in a restriction. Exercise 13 of
[TakeutiZaring] p. 25.
(Contributed by NM, 14Oct2005.)



Theorem  brresg 4620 
Binary relation on a restriction. (Contributed by Mario Carneiro,
4Nov2015.)



Theorem  opres 4621 
Ordered pair membership in a restriction when the first member belongs
to the restricting class. (Contributed by NM, 30Apr2004.) (Proof
shortened by Andrew Salmon, 27Aug2011.)



Theorem  resieq 4622 
A restricted identity relation is equivalent to equality in its domain.
(Contributed by NM, 30Apr2004.)



Theorem  opelresi 4623 
belongs to a restriction of the identity class iff
belongs to the restricting class. (Contributed by FL, 27Oct2008.)
(Revised by NM, 30Mar2016.)



Theorem  resres 4624 
The restriction of a restriction. (Contributed by NM, 27Mar2008.)



Theorem  resundi 4625 
Distributive law for restriction over union. Theorem 31 of [Suppes]
p. 65. (Contributed by NM, 30Sep2002.)



Theorem  resundir 4626 
Distributive law for restriction over union. (Contributed by NM,
23Sep2004.)



Theorem  resindi 4627 
Class restriction distributes over intersection. (Contributed by FL,
6Oct2008.)



Theorem  resindir 4628 
Class restriction distributes over intersection. (Contributed by NM,
18Dec2008.)



Theorem  inres 4629 
Move intersection into class restriction. (Contributed by NM,
18Dec2008.)



Theorem  resiun1 4630* 
Distribution of restriction over indexed union. (Contributed by Mario
Carneiro, 29May2015.)



Theorem  resiun2 4631* 
Distribution of restriction over indexed union. (Contributed by Mario
Carneiro, 29May2015.)



Theorem  dmres 4632 
The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25.
(Contributed by NM, 1Aug1994.)



Theorem  ssdmres 4633 
A domain restricted to a subclass equals the subclass. (Contributed by
NM, 2Mar1997.)



Theorem  dmresexg 4634 
The domain of a restriction to a set exists. (Contributed by NM,
7Apr1995.)



Theorem  resss 4635 
A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25.
(Contributed by NM, 2Aug1994.)



Theorem  rescom 4636 
Commutative law for restriction. (Contributed by NM, 27Mar1998.)



Theorem  ssres 4637 
Subclass theorem for restriction. (Contributed by NM, 16Aug1994.)



Theorem  ssres2 4638 
Subclass theorem for restriction. (Contributed by NM, 22Mar1998.)
(Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  relres 4639 
A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25.
(Contributed by NM, 2Aug1994.) (Proof shortened by Andrew Salmon,
27Aug2011.)



Theorem  resabs1 4640 
Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25.
(Contributed by NM, 9Aug1994.)



Theorem  resabs2 4641 
Absorption law for restriction. (Contributed by NM, 27Mar1998.)



Theorem  residm 4642 
Idempotent law for restriction. (Contributed by NM, 27Mar1998.)



Theorem  resima 4643 
A restriction to an image. (Contributed by NM, 29Sep2004.)



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



Theorem  xpssres 4645 
Restriction of a constant function (or other cross product). (Contributed
by Stefan O'Rear, 24Jan2015.)



Theorem  elres 4646* 
Membership in a restriction. (Contributed by Scott Fenton,
17Mar2011.)



Theorem  elsnres 4647* 
Memebership in restriction to a singleton. (Contributed by Scott
Fenton, 17Mar2011.)



Theorem  relssres 4648 
Simplification law for restriction. (Contributed by NM,
16Aug1994.)



Theorem  resdm 4649 
A relation restricted to its domain equals itself. (Contributed by NM,
12Dec2006.)



Theorem  resexg 4650 
The restriction of a set is a set. (Contributed by NM, 28Mar1998.)
(Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  resex 4651 
The restriction of a set is a set. (Contributed by Jeff Madsen,
19Jun2011.)



Theorem  resopab 4652* 
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 5Nov2002.)



Theorem  resiexg 4653 
The existence of a restricted identity function, proved without using
the Axiom of Replacement. (Contributed by NM, 13Jan2007.)



Theorem  iss 4654 
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 4655* 
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 24Aug2007.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

Se


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

Se 

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

