Type  Label  Description 
Statement 

Theorem  csbdmg 4701 
Distribute proper substitution through the domain of a class.
(Contributed by Jim Kingdon, 8Dec2018.)



Theorem  eldmg 4702* 
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  eldm2g 4703* 
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by NM,
27Jan1997.) (Revised by Mario Carneiro, 9Jul2014.)



Theorem  eldm 4704* 
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 2Apr2004.)



Theorem  eldm2 4705* 
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 1Aug1994.)



Theorem  dmss 4706 
Subset theorem for domain. (Contributed by NM, 11Aug1994.)



Theorem  dmeq 4707 
Equality theorem for domain. (Contributed by NM, 11Aug1994.)



Theorem  dmeqi 4708 
Equality inference for domain. (Contributed by NM, 4Mar2004.)



Theorem  dmeqd 4709 
Equality deduction for domain. (Contributed by NM, 4Mar2004.)



Theorem  opeldm 4710 
Membership of first of an ordered pair in a domain. (Contributed by NM,
30Jul1995.)



Theorem  breldm 4711 
Membership of first of a binary relation in a domain. (Contributed by
NM, 30Jul1995.)



Theorem  opeldmg 4712 
Membership of first of an ordered pair in a domain. (Contributed by Jim
Kingdon, 9Jul2019.)



Theorem  breldmg 4713 
Membership of first of a binary relation in a domain. (Contributed by
NM, 21Mar2007.)



Theorem  dmun 4714 
The domain of a union is the union of domains. Exercise 56(a) of
[Enderton] p. 65. (Contributed by NM,
12Aug1994.) (Proof shortened
by Andrew Salmon, 27Aug2011.)



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



Theorem  dmiun 4716 
The domain of an indexed union. (Contributed by Mario Carneiro,
26Apr2016.)



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



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



Theorem  dmopabss 4719* 
Upper bound for the domain of a restricted class of ordered pairs.
(Contributed by NM, 31Jan2004.)



Theorem  dmopab3 4720* 
The domain of a restricted class of ordered pairs. (Contributed by NM,
31Jan2004.)



Theorem  dm0 4721 
The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1]
p. 36. (Contributed by NM, 4Jul1994.) (Proof shortened by Andrew
Salmon, 27Aug2011.)



Theorem  dmi 4722 
The domain of the identity relation is the universe. (Contributed by
NM, 30Apr1998.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  dmv 4723 
The domain of the universe is the universe. (Contributed by NM,
8Aug2003.)



Theorem  dm0rn0 4724 
An empty domain implies an empty range. For a similar theorem for
whether the domain and range are inhabited, see dmmrnm 4726. (Contributed
by NM, 21May1998.)



Theorem  reldm0 4725 
A relation is empty iff its domain is empty. (Contributed by NM,
15Sep2004.)



Theorem  dmmrnm 4726* 
A domain is inhabited if and only if the range is inhabited.
(Contributed by Jim Kingdon, 15Dec2018.)



Theorem  dmxpm 4727* 
The domain of a cross product. Part of Theorem 3.13(x) of [Monk1]
p. 37. (Contributed by NM, 28Jul1995.) (Proof shortened by Andrew
Salmon, 27Aug2011.)



Theorem  dmxpid 4728 
The domain of a square Cartesian product. (Contributed by NM,
28Jul1995.) (Revised by Jim Kingdon, 11Apr2023.)



Theorem  dmxpin 4729 
The domain of the intersection of two square Cartesian products. Unlike
dmin 4715, equality holds. (Contributed by NM,
29Jan2008.)



Theorem  xpid11 4730 
The Cartesian product of a class with itself is onetoone. (Contributed
by NM, 5Nov2006.) (Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  dmcnvcnv 4731 
The domain of the double converse of a class (which doesn't have to be a
relation as in dfrel2 4957). (Contributed by NM, 8Apr2007.)



Theorem  rncnvcnv 4732 
The range of the double converse of a class. (Contributed by NM,
8Apr2007.)



Theorem  elreldm 4733 
The first member of an ordered pair in a relation belongs to the domain
of the relation. (Contributed by NM, 28Jul2004.)



Theorem  rneq 4734 
Equality theorem for range. (Contributed by NM, 29Dec1996.)



Theorem  rneqi 4735 
Equality inference for range. (Contributed by NM, 4Mar2004.)



Theorem  rneqd 4736 
Equality deduction for range. (Contributed by NM, 4Mar2004.)



Theorem  rnss 4737 
Subset theorem for range. (Contributed by NM, 22Mar1998.)



Theorem  brelrng 4738 
The second argument of a binary relation belongs to its range.
(Contributed by NM, 29Jun2008.)



Theorem  opelrng 4739 
Membership of second member of an ordered pair in a range. (Contributed
by Jim Kingdon, 26Jan2019.)



Theorem  brelrn 4740 
The second argument of a binary relation belongs to its range.
(Contributed by NM, 13Aug2004.)



Theorem  opelrn 4741 
Membership of second member of an ordered pair in a range. (Contributed
by NM, 23Feb1997.)



Theorem  releldm 4742 
The first argument of a binary relation belongs to its domain.
(Contributed by NM, 2Jul2008.)



Theorem  relelrn 4743 
The second argument of a binary relation belongs to its range.
(Contributed by NM, 2Jul2008.)



Theorem  releldmb 4744* 
Membership in a domain. (Contributed by Mario Carneiro, 5Nov2015.)



Theorem  relelrnb 4745* 
Membership in a range. (Contributed by Mario Carneiro, 5Nov2015.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  elrnmptdv 4761* 
Elementhood in the range of a function in mapsto notation, deduction
form. (Contributed by Rohan Ridenour, 3Aug2023.)



Theorem  elrnmpt2d 4762* 
Elementhood in the range of a function in mapsto notation, deduction
form. (Contributed by Rohan Ridenour, 3Aug2023.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

