Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

