Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  resdmdfsn 4742 
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 4743* 
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 5Nov2002.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

Se


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

Se 

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



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



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



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



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



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



Theorem  cotr 4800* 
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.)

