Type  Label  Description 
Statement 

Theorem  nfco 4501 
Boundvariable hypothesis builder for function value. (Contributed by
NM, 1Sep1999.)



Theorem  brcog 4502* 
Ordered pair membership in a composition. (Contributed by NM,
24Feb2015.)



Theorem  opelco2g 4503* 
Ordered pair membership in a composition. (Contributed by NM,
27Jan1997.) (Revised by Mario Carneiro, 24Feb2015.)



Theorem  brcogw 4504 
Ordered pair membership in a composition. (Contributed by Thierry
Arnoux, 14Jan2018.)



Theorem  eqbrrdva 4505* 
Deduction from extensionality principle for relations, given an
equivalence only on the relation's domain and range. (Contributed by
Thierry Arnoux, 28Nov2017.)



Theorem  brco 4506* 
Binary relation on a composition. (Contributed by NM, 21Sep2004.)
(Revised by Mario Carneiro, 24Feb2015.)



Theorem  opelco 4507* 
Ordered pair membership in a composition. (Contributed by NM,
27Dec1996.) (Revised by Mario Carneiro, 24Feb2015.)



Theorem  cnvss 4508 
Subset theorem for converse. (Contributed by NM, 22Mar1998.)



Theorem  cnveq 4509 
Equality theorem for converse. (Contributed by NM, 13Aug1995.)



Theorem  cnveqi 4510 
Equality inference for converse. (Contributed by NM, 23Dec2008.)



Theorem  cnveqd 4511 
Equality deduction for converse. (Contributed by NM, 6Dec2013.)



Theorem  elcnv 4512* 
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 24Mar1998.)



Theorem  elcnv2 4513* 
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 11Aug2004.)



Theorem  nfcnv 4514 
Boundvariable hypothesis builder for converse. (Contributed by NM,
31Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  opelcnvg 4515 
Orderedpair membership in converse. (Contributed by NM, 13May1999.)
(Proof shortened by Andrew Salmon, 27Aug2011.)



Theorem  brcnvg 4516 
The converse of a binary relation swaps arguments. Theorem 11 of [Suppes]
p. 61. (Contributed by NM, 10Oct2005.)



Theorem  opelcnv 4517 
Orderedpair membership in converse. (Contributed by NM,
13Aug1995.)



Theorem  brcnv 4518 
The converse of a binary relation swaps arguments. Theorem 11 of
[Suppes] p. 61. (Contributed by NM,
13Aug1995.)



Theorem  csbcnvg 4519 
Move class substitution in and out of the converse of a function.
(Contributed by Thierry Arnoux, 8Feb2017.)



Theorem  cnvco 4520 
Distributive law of converse over class composition. Theorem 26 of
[Suppes] p. 64. (Contributed by NM,
19Mar1998.) (Proof shortened by
Andrew Salmon, 27Aug2011.)



Theorem  cnvuni 4521* 
The converse of a class union is the (indexed) union of the converses of
its members. (Contributed by NM, 11Aug2004.)



Theorem  dfdm3 4522* 
Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring]
p. 24. (Contributed by NM, 28Dec1996.)



Theorem  dfrn2 4523* 
Alternate definition of range. Definition 4 of [Suppes] p. 60.
(Contributed by NM, 27Dec1996.)



Theorem  dfrn3 4524* 
Alternate definition of range. Definition 6.5(2) of [TakeutiZaring]
p. 24. (Contributed by NM, 28Dec1996.)



Theorem  elrn2g 4525* 
Membership in a range. (Contributed by Scott Fenton, 2Feb2011.)



Theorem  elrng 4526* 
Membership in a range. (Contributed by Scott Fenton, 2Feb2011.)



Theorem  dfdm4 4527 
Alternate definition of domain. (Contributed by NM, 28Dec1996.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  rnex 4599 
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 4600 
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.)

