Type  Label  Description 
Statement 

Theorem  releldmi 4601 
The first argument of a binary relation belongs to its domain.
(Contributed by NM, 28Apr2015.)



Theorem  relelrni 4602 
The second argument of a binary relation belongs to its range.
(Contributed by NM, 28Apr2015.)



Theorem  dfrnf 4603* 
Definition of range, using boundvariable hypotheses instead of distinct
variable conditions. (Contributed by NM, 14Aug1995.) (Revised by
Mario Carneiro, 15Oct2016.)



Theorem  elrn2 4604* 
Membership in a range. (Contributed by NM, 10Jul1994.)



Theorem  elrn 4605* 
Membership in a range. (Contributed by NM, 2Apr2004.)



Theorem  nfdm 4606 
Boundvariable hypothesis builder for domain. (Contributed by NM,
30Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  nfrn 4607 
Boundvariable hypothesis builder for range. (Contributed by NM,
1Sep1999.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  dmiin 4608 
Domain of an intersection. (Contributed by FL, 15Oct2012.)



Theorem  rnopab 4609* 
The range of a class of ordered pairs. (Contributed by NM,
14Aug1995.) (Revised by Mario Carneiro, 4Dec2016.)



Theorem  rnmpt 4610* 
The range of a function in mapsto notation. (Contributed by Scott
Fenton, 21Mar2011.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  elrnmpt 4611* 
The range of a function in mapsto notation. (Contributed by Mario
Carneiro, 20Feb2015.)



Theorem  elrnmpt1s 4612* 
Elementhood in an image set. (Contributed by Mario Carneiro,
12Sep2015.)



Theorem  elrnmpt1 4613 
Elementhood in an image set. (Contributed by Mario Carneiro,
31Aug2015.)



Theorem  elrnmptg 4614* 
Membership in the range of a function. (Contributed by NM,
27Aug2007.) (Revised by Mario Carneiro, 31Aug2015.)



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



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



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



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



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



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



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



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



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



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



Theorem  rnexg 4625 
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 4626 
The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring]
p. 26. (Contributed by NM, 7Jul2008.)



Theorem  rnex 4627 
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 4628 
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 4629 
Domain of a composition. Theorem 21 of [Suppes]
p. 63. (Contributed by
NM, 19Mar1998.) (Proof shortened by Andrew Salmon, 27Aug2011.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

