Type  Label  Description 
Statement 

Theorem  dfdm3 4901* 
Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring]
p. 24. (Contributed by set.mm contributors, 28Dec1996.)



Theorem  dfrn2 4902* 
Alternate definition of range. Definition 4 of [Suppes] p. 60.
(Contributed by set.mm contributors, 27Dec1996.)



Theorem  dfrn3 4903* 
Alternate definition of range. Definition 6.5(2) of [TakeutiZaring]
p. 24. (Contributed by set.mm contributors, 28Dec1996.)



Theorem  dfrn4 4904 
Alternate definition of range. (Contributed by set.mm contributors,
5Feb2015.)



Theorem  dfdmf 4905* 
Definition of domain, using boundvariable hypotheses instead of
distinct variable conditions. (Contributed by NM, 8Mar1995.)
(Revised by Mario Carneiro, 15Oct2016.)



Theorem  dmss 4906 
Subset theorem for domain. (Contributed by set.mm contributors,
11Aug1994.)



Theorem  dmeq 4907 
Equality theorem for domain. (Contributed by set.mm contributors,
11Aug1994.)



Theorem  dmeqi 4908 
Equality inference for domain. (Contributed by set.mm contributors,
4Mar2004.)



Theorem  dmeqd 4909 
Equality deduction for domain. (Contributed by set.mm contributors,
4Mar2004.)



Theorem  opeldm 4910 
Membership of first of an ordered pair in a domain. (Contributed by
set.mm contributors, 30Jul1995.)



Theorem  breldm 4911 
Membership of first of a binary relation in a domain. (Contributed by
set.mm contributors, 8Jan2015.)



Theorem  dmun 4912 
The domain of a union is the union of domains. Exercise 56(a) of
[Enderton] p. 65. (The proof was
shortened by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 12Aug1994.)
(Revised by set.mm contributors, 27Aug2011.)



Theorem  dmin 4913 
The domain of an intersection belong to the intersection of domains.
Theorem 6 of [Suppes] p. 60.
(Contributed by set.mm contributors,
15Sep2004.)



Theorem  dmuni 4914* 
The domain of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by set.mm contributors, 3Feb2004.)



Theorem  dmopab 4915* 
The domain of a class of ordered pairs. (Contributed by NM,
16May1995.) (Revised by Mario Carneiro, 4Dec2016.)



Theorem  dmopabss 4916* 
Upper bound for the domain of a restricted class of ordered pairs.
(Contributed by set.mm contributors, 31Jan2004.)



Theorem  dmopab3 4917* 
The domain of a restricted class of ordered pairs. (Contributed by
set.mm contributors, 31Jan2004.)



Theorem  dm0 4918 
The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
p. 36. (The proof was shortened by Andrew Salmon, 27Aug2011.)
(Contributed by set.mm contributors, 4Jul1994.) (Revised by set.mm
contributors, 27Aug2011.)



Theorem  dmi 4919 
The domain of the identity relation is the universe. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 30Apr1998.) (Revised by set.mm contributors,
27Aug2011.)



Theorem  dmv 4920 
The domain of the universe is the universe. (Contributed by set.mm
contributors, 8Aug2003.)



Theorem  dm0rn0 4921 
An empty domain implies an empty range. (Contributed by set.mm
contributors, 21May1998.)



Theorem  dmeq0 4922 
A class is empty iff its domain is empty. (Contributed by set.mm
contributors, 15Sep2004.) (Revised by Scott Fenton, 17Apr2021.)



Theorem  dmxp 4923 
The domain of a cross product. Part of Theorem 3.13(x) of [Monk1]
p. 37. (The proof was shortened by Andrew Salmon, 27Aug2011.)
(Contributed by set.mm contributors, 28Jul1995.) (Revised by set.mm
contributors, 27Aug2011.)



Theorem  dmxpid 4924 
The domain of a square cross product. (Contributed by set.mm
contributors, 28Jul1995.)



Theorem  dmxpin 4925 
The domain of the intersection of two square cross products. Unlike
dmin 4913, equality holds. (Contributed by set.mm
contributors,
29Jan2008.)



Theorem  xpid11 4926 
The cross product of a class with itself is onetoone. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 5Nov2006.) (Revised by set.mm contributors,
27Aug2011.)



Theorem  proj1eldm 4927 
The first member of an ordered pair in a class belongs to the domain
of the class. (Contributed by set.mm contributors, 28Jul2004.)
(Revised by Scott Fenton, 18Apr2021.)

Proj1 

Theorem  reseq1 4928 
Equality theorem for restrictions. (Contributed by set.mm contributors,
7Aug1994.)



Theorem  reseq2 4929 
Equality theorem for restrictions. (Contributed by set.mm contributors,
8Aug1994.)



Theorem  reseq1i 4930 
Equality inference for restrictions. (Contributed by set.mm
contributors, 21Oct2014.)



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



Theorem  reseq12i 4932 
Equality inference for restrictions. (Contributed by set.mm
contributors, 21Oct2014.)



Theorem  reseq1d 4933 
Equality deduction for restrictions. (Contributed by set.mm
contributors, 21Oct2014.)



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



Theorem  reseq12d 4935 
Equality deduction for restrictions. (Contributed by set.mm
contributors, 21Oct2014.)



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



Theorem  imaeq1 4937 
Equality theorem for image. (Contributed by set.mm contributors,
14Aug1994.)



Theorem  imaeq2 4938 
Equality theorem for image. (Contributed by set.mm contributors,
14Aug1994.)



Theorem  imaeq1i 4939 
Equality theorem for image. (Contributed by set.mm contributors,
21Dec2008.)



Theorem  imaeq2i 4940 
Equality theorem for image. (Contributed by set.mm contributors,
21Dec2008.)



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



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



Theorem  imaeq12d 4943 
Equality theorem for image. (Contributed by SF, 8Jan2018.)



Theorem  elimapw1 4944* 
Membership in an image under a unit power class. (Contributed by set.mm
contributors, 19Feb2015.)

_{1}


Theorem  elimapw12 4945* 
Membership in an image under two unit power classes. (Contributed by
set.mm contributors, 18Mar2015.)

_{1} _{1} 

Theorem  elimapw13 4946* 
Membership in an image under three unit power classes. (Contributed by
set.mm contributors, 18Mar2015.)

_{1} _{1} _{1} 

Theorem  elima1c 4947* 
Membership in an image under cardinal one. (Contributed by set.mm
contributors, 6Feb2015.)

1_{c} 

Theorem  elimapw11c 4948* 
Membership in an image under the unit power class of cardinal one.
(Contributed by set.mm contributors, 25Feb2015.)

_{1} 1_{c} 

Theorem  brres 4949 
Binary relation on a restriction. (Contributed by set.mm contributors,
12Dec2006.)



Theorem  opelres 4950 
Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring]
p. 25. (Contributed by set.mm contributors, 13Nov1995.)



Theorem  dfima3 4951 
Alternate definition of image. (Contributed by set.mm contributors,
19Apr2004.) (Revised by set.mm contributors, 27Aug2011.)



Theorem  dfima4 4952* 
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (The proof was shortened by Andrew Salmon, 27Aug2011.)
(Contributed by set.mm contributors, 14Aug1994.) (Revised by set.mm
contributors, 27Aug2011.)



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



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



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



Theorem  rneq 4956 
Equality theorem for range. (Contributed by set.mm contributors,
29Dec1996.)



Theorem  rneqi 4957 
Equality inference for range. (Contributed by set.mm contributors,
4Mar2004.)



Theorem  rneqd 4958 
Equality deduction for range. (Contributed by set.mm contributors,
4Mar2004.)



Theorem  rnss 4959 
Subset theorem for range. (Contributed by set.mm contributors,
22Mar1998.)



Theorem  brelrn 4960 
The second argument of a binary relation belongs to its range.
(Contributed by set.mm contributors, 29Jun2008.)



Theorem  opelrn 4961 
Membership of second member of an ordered pair in a range. (Contributed
by set.mm contributors, 8Jan2015.)



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



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



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



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



Theorem  csbrng 4966 
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10Nov2012.)



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



Theorem  rnopab2 4968* 
The range of a function expressed as a class abstraction. (Contributed
by set.mm contributors, 23Mar2006.)



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



Theorem  rneq0 4970 
A relation is empty iff its range is empty. (Contributed by set.mm
contributors, 15Sep2004.) (Revised by Scott Fenton, 17Apr2021.)



Theorem  dmcoss 4971 
Domain of a composition. Theorem 21 of [Suppes]
p. 63. (The proof was
shortened by Andrew Salmon, 27Aug2011.) (Contributed by set.mm
contributors, 19Mar1998.) (Revised by set.mm contributors,
27Aug2011.)



Theorem  rncoss 4972 
Range of a composition. (Contributed by set.mm contributors,
19Mar1998.)



Theorem  dmcosseq 4973 
Domain of a composition. (The proof was shortened by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 28May1998.)
(Revised by set.mm contributors, 27Aug2011.)



Theorem  dmcoeq 4974 
Domain of a composition. (Contributed by set.mm contributors,
19Mar1998.)



Theorem  rncoeq 4975 
Range of a composition. (Contributed by set.mm contributors,
19Mar1998.)



Theorem  csbresg 4976 
Distribute proper substitution through the restriction of a class.
csbresg 4976 is derived from the virtual deduction proof
csbresgVD in
set.mm. (Contributed by Alan Sare, 10Nov2012.)



Theorem  res0 4977 
A restriction to the empty set is empty. (Contributed by set.mm
contributors, 12Nov1994.)



Theorem  opres 4978 
Ordered pair membership in a restriction when the first member belongs to
the restricting class. (The proof was shortened by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 30Apr2004.)
(Revised by set.mm contributors, 27Aug2011.)



Theorem  resieq 4979 
A restricted identity relation is equivalent to equality in its domain.
(Contributed by set.mm contributors, 30Apr2004.)



Theorem  resres 4980 
The restriction of a restriction. (Contributed by set.mm contributors,
27Mar2008.)



Theorem  resundi 4981 
Distributive law for restriction over union. Theorem 31 of [Suppes]
p. 65. (Contributed by set.mm contributors, 30Sep2002.)



Theorem  resundir 4982 
Distributive law for restriction over union. (Contributed by set.mm
contributors, 23Sep2004.)



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



Theorem  resindir 4984 
Class restriction distributes over intersection. (Contributed by set.mm
contributors, 18Dec2008.)



Theorem  inres 4985 
Move intersection into class restriction. (Contributed by set.mm
contributors, 18Dec2008.)



Theorem  dmres 4986 
The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 1Aug1994.)



Theorem  ssdmres 4987 
A domain restricted to a subclass equals the subclass. (Contributed by
set.mm contributors, 2Mar1997.) (Revised by set.mm contributors,
28Aug2004.)



Theorem  resss 4988 
A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 2Aug1994.)



Theorem  rescom 4989 
Commutative law for restriction. (Contributed by set.mm contributors,
27Mar1998.)



Theorem  ssres 4990 
Subclass theorem for restriction. (Contributed by set.mm contributors,
16Aug1994.)



Theorem  ssres2 4991 
Subclass theorem for restriction. (The proof was shortened by Andrew
Salmon, 27Aug2011.) (Contributed by set.mm contributors, 22Mar1998.)
(Revised by set.mm contributors, 27Aug2011.)



Theorem  resabs1 4992 
Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25.
(Contributed by set.mm contributors, 9Aug1994.)



Theorem  resabs2 4993 
Absorption law for restriction. (Contributed by set.mm contributors,
27Mar1998.)



Theorem  residm 4994 
Idempotent law for restriction. (Contributed by set.mm contributors,
27Mar1998.)



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



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



Theorem  ssreseq 4997 
Simplification law for restriction. (Contributed by set.mm
contributors, 16Aug1994.) (Revised by set.mm contributors,
15Mar2004.) (Revised by Scott Fenton, 18Apr2021.)



Theorem  resdm 4998 
A class restricted to its domain equals itself. (Contributed by set.mm
contributors, 12Dec2006.) (Revised by Scott Fenton, 18Apr2021.)



Theorem  resopab 4999* 
Restriction of a class abstraction of ordered pairs. (Contributed by
set.mm contributors, 5Nov2002.)



Theorem  iss 5000 
A subclass of the identity function is the identity function restricted
to its domain. (The proof was shortened by Andrew Salmon,
27Aug2011.) (Contributed by set.mm contributors, 13Dec2003.)
(Revised by set.mm contributors, 27Aug2011.)

