Type  Label  Description 
Statement 

Theorem  elrnmpti 4701* 
Membership in the range of a function. (Contributed by NM,
30Aug2004.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  rn0 4702 
The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
p. 36. (Contributed by NM, 4Jul1994.)



Theorem  dfiun3g 4703 
Alternate definition of indexed union when is a set. (Contributed
by Mario Carneiro, 31Aug2015.)



Theorem  dfiin3g 4704 
Alternate definition of indexed intersection when is a set.
(Contributed by Mario Carneiro, 31Aug2015.)



Theorem  dfiun3 4705 
Alternate definition of indexed union when is a set. (Contributed
by Mario Carneiro, 31Aug2015.)



Theorem  dfiin3 4706 
Alternate definition of indexed intersection when is a set.
(Contributed by Mario Carneiro, 31Aug2015.)



Theorem  riinint 4707* 
Express a relative indexed intersection as an intersection.
(Contributed by Stefan O'Rear, 22Feb2015.)



Theorem  relrn0 4708 
A relation is empty iff its range is empty. (Contributed by NM,
15Sep2004.)



Theorem  dmrnssfld 4709 
The domain and range of a class are included in its double union.
(Contributed by NM, 13May2008.)



Theorem  dmexg 4710 
The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26.
(Contributed by NM, 7Apr1995.)



Theorem  rnexg 4711 
The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26.
Similar to Lemma 3D of [Enderton] p. 41.
(Contributed by NM,
31Mar1995.)



Theorem  dmex 4712 
The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring]
p. 26. (Contributed by NM, 7Jul2008.)



Theorem  rnex 4713 
The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26.
Similar to Lemma 3D of [Enderton] p.
41. (Contributed by NM,
7Jul2008.)



Theorem  iprc 4714 
The identity function is a proper class. This means, for example, that we
cannot use it as a member of the class of continuous functions unless it
is restricted to a set. (Contributed by NM, 1Jan2007.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  opres 4735 
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 4736 
A restricted identity relation is equivalent to equality in its domain.
(Contributed by NM, 30Apr2004.)



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



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



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



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



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



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



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



Theorem  resdifcom 4744 
Commutative law for restriction and difference. (Contributed by AV,
7Jun2021.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  resindm 4767 
When restricting a relation, intersecting with the domain of the relation
has no effect. (Contributed by FL, 6Oct2008.)



Theorem  resdmdfsn 4768 
Restricting a relation to its domain without a set is the same as
restricting the relation to the universe without this set. (Contributed
by AV, 2Dec2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

