Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



Theorem  dmun 4611 
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 4612 
The domain of an intersection belong to the intersection of domains.
Theorem 6 of [Suppes] p. 60.
(Contributed by NM, 15Sep2004.)



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



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



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



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



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



Theorem  dm0 4618 
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 4619 
The domain of the identity relation is the universe. (Contributed by
NM, 30Apr1998.) (Proof shortened by Andrew Salmon, 27Aug2011.)



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



Theorem  dm0rn0 4621 
An empty domain implies an empty range. (Contributed by NM,
21May1998.)



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



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



Theorem  dmxpm 4624* 
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  dmxpinm 4625* 
The domain of the intersection of two square cross products. Unlike
dmin 4612, equality holds. (Contributed by NM,
29Jan2008.)



Theorem  xpid11m 4626* 
The cross product of a class with itself is onetoone. (Contributed by
Jim Kingdon, 8Dec2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

