Type  Label  Description 
Statement 

Theorem  f1co 5101 
Composition of onetoone functions. Exercise 30 of [TakeutiZaring]
p. 25. (Contributed by NM, 28May1998.)



Theorem  foeq1 5102 
Equality theorem for onto functions. (Contributed by NM, 1Aug1994.)



Theorem  foeq2 5103 
Equality theorem for onto functions. (Contributed by NM, 1Aug1994.)



Theorem  foeq3 5104 
Equality theorem for onto functions. (Contributed by NM, 1Aug1994.)



Theorem  nffo 5105 
Boundvariable hypothesis builder for an onto function. (Contributed by
NM, 16May2004.)



Theorem  fof 5106 
An onto mapping is a mapping. (Contributed by NM, 3Aug1994.)



Theorem  fofun 5107 
An onto mapping is a function. (Contributed by NM, 29Mar2008.)



Theorem  fofn 5108 
An onto mapping is a function on its domain. (Contributed by NM,
16Dec2008.)



Theorem  forn 5109 
The codomain of an onto function is its range. (Contributed by NM,
3Aug1994.)



Theorem  dffo2 5110 
Alternate definition of an onto function. (Contributed by NM,
22Mar2006.)



Theorem  foima 5111 
The image of the domain of an onto function. (Contributed by NM,
29Nov2002.)



Theorem  dffn4 5112 
A function maps onto its range. (Contributed by NM, 10May1998.)



Theorem  funforn 5113 
A function maps its domain onto its range. (Contributed by NM,
23Jul2004.)



Theorem  fodmrnu 5114 
An onto function has unique domain and range. (Contributed by NM,
5Nov2006.)



Theorem  fores 5115 
Restriction of a function. (Contributed by NM, 4Mar1997.)



Theorem  foco 5116 
Composition of onto functions. (Contributed by NM, 22Mar2006.)



Theorem  f1oeq1 5117 
Equality theorem for onetoone onto functions. (Contributed by NM,
10Feb1997.)



Theorem  f1oeq2 5118 
Equality theorem for onetoone onto functions. (Contributed by NM,
10Feb1997.)



Theorem  f1oeq3 5119 
Equality theorem for onetoone onto functions. (Contributed by NM,
10Feb1997.)



Theorem  f1oeq23 5120 
Equality theorem for onetoone onto functions. (Contributed by FL,
14Jul2012.)



Theorem  f1eq123d 5121 
Equality deduction for onetoone functions. (Contributed by Mario
Carneiro, 27Jan2017.)



Theorem  foeq123d 5122 
Equality deduction for onto functions. (Contributed by Mario Carneiro,
27Jan2017.)



Theorem  f1oeq123d 5123 
Equality deduction for onetoone onto functions. (Contributed by Mario
Carneiro, 27Jan2017.)



Theorem  nff1o 5124 
Boundvariable hypothesis builder for a onetoone onto function.
(Contributed by NM, 16May2004.)



Theorem  f1of1 5125 
A onetoone onto mapping is a onetoone mapping. (Contributed by NM,
12Dec2003.)



Theorem  f1of 5126 
A onetoone onto mapping is a mapping. (Contributed by NM,
12Dec2003.)



Theorem  f1ofn 5127 
A onetoone onto mapping is function on its domain. (Contributed by NM,
12Dec2003.)



Theorem  f1ofun 5128 
A onetoone onto mapping is a function. (Contributed by NM,
12Dec2003.)



Theorem  f1orel 5129 
A onetoone onto mapping is a relation. (Contributed by NM,
13Dec2003.)



Theorem  f1odm 5130 
The domain of a onetoone onto mapping. (Contributed by NM,
8Mar2014.)



Theorem  dff1o2 5131 
Alternate definition of onetoone onto function. (Contributed by NM,
10Feb1997.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  dff1o3 5132 
Alternate definition of onetoone onto function. (Contributed by NM,
25Mar1998.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  f1ofo 5133 
A onetoone onto function is an onto function. (Contributed by NM,
28Apr2004.)



Theorem  dff1o4 5134 
Alternate definition of onetoone onto function. (Contributed by NM,
25Mar1998.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  dff1o5 5135 
Alternate definition of onetoone onto function. (Contributed by NM,
10Dec2003.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  f1orn 5136 
A onetoone function maps onto its range. (Contributed by NM,
13Aug2004.)



Theorem  f1f1orn 5137 
A onetoone function maps onetoone onto its range. (Contributed by NM,
4Sep2004.)



Theorem  f1oabexg 5138* 
The class of all 11onto functions mapping one set to another is a set.
(Contributed by Paul Chapman, 25Feb2008.)



Theorem  f1ocnv 5139 
The converse of a onetoone onto function is also onetoone onto.
(Contributed by NM, 11Feb1997.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  f1ocnvb 5140 
A relation is a onetoone onto function iff its converse is a onetoone
onto function with domain and range interchanged. (Contributed by NM,
8Dec2003.)



Theorem  f1ores 5141 
The restriction of a onetoone function maps onetoone onto the image.
(Contributed by NM, 25Mar1998.)



Theorem  f1orescnv 5142 
The converse of a onetooneonto restricted function. (Contributed by
Paul Chapman, 21Apr2008.)



Theorem  f1imacnv 5143 
Preimage of an image. (Contributed by NM, 30Sep2004.)



Theorem  foimacnv 5144 
A reverse version of f1imacnv 5143. (Contributed by Jeff Hankins,
16Jul2009.)



Theorem  foun 5145 
The union of two onto functions with disjoint domains is an onto function.
(Contributed by Mario Carneiro, 22Jun2016.)



Theorem  f1oun 5146 
The union of two onetoone onto functions with disjoint domains and
ranges. (Contributed by NM, 26Mar1998.)



Theorem  fun11iun 5147* 
The union of a chain (with respect to inclusion) of onetoone functions
is a onetoone function. (Contributed by Mario Carneiro, 20May2013.)
(Revised by Mario Carneiro, 24Jun2015.)



Theorem  resdif 5148 
The restriction of a onetoone onto function to a difference maps onto
the difference of the images. (Contributed by Paul Chapman,
11Apr2009.)



Theorem  f1oco 5149 
Composition of onetoone onto functions. (Contributed by NM,
19Mar1998.)



Theorem  f1cnv 5150 
The converse of an injective function is bijective. (Contributed by FL,
11Nov2011.)



Theorem  funcocnv2 5151 
Composition with the converse. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  fococnv2 5152 
The composition of an onto function and its converse. (Contributed by
Stefan O'Rear, 12Feb2015.)



Theorem  f1ococnv2 5153 
The composition of a onetoone onto function and its converse equals the
identity relation restricted to the function's range. (Contributed by NM,
13Dec2003.) (Proof shortened by Stefan O'Rear, 12Feb2015.)



Theorem  f1cocnv2 5154 
Composition of an injective function with its converse. (Contributed by
FL, 11Nov2011.)



Theorem  f1ococnv1 5155 
The composition of a onetoone onto function's converse and itself equals
the identity relation restricted to the function's domain. (Contributed
by NM, 13Dec2003.)



Theorem  f1cocnv1 5156 
Composition of an injective function with its converse. (Contributed by
FL, 11Nov2011.)



Theorem  funcoeqres 5157 
Reexpress a constraint on a composition as a constraint on the composand.
(Contributed by Stefan O'Rear, 7Mar2015.)



Theorem  ffoss 5158* 
Relationship between a mapping and an onto mapping. Figure 38 of
[Enderton] p. 145. (Contributed by NM,
10May1998.)



Theorem  f11o 5159* 
Relationship between onetoone and onetoone onto function.
(Contributed by NM, 4Apr1998.)



Theorem  f10 5160 
The empty set maps onetoone into any class. (Contributed by NM,
7Apr1998.)



Theorem  f1o00 5161 
Onetoone onto mapping of the empty set. (Contributed by NM,
15Apr1998.)



Theorem  fo00 5162 
Onto mapping of the empty set. (Contributed by NM, 22Mar2006.)



Theorem  f1o0 5163 
Onetoone onto mapping of the empty set. (Contributed by NM,
10Sep2004.)



Theorem  f1oi 5164 
A restriction of the identity relation is a onetoone onto function.
(Contributed by NM, 30Apr1998.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  f1ovi 5165 
The identity relation is a onetoone onto function on the universe.
(Contributed by NM, 16May2004.)



Theorem  f1osn 5166 
A singleton of an ordered pair is onetoone onto function.
(Contributed by NM, 18May1998.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  f1osng 5167 
A singleton of an ordered pair is onetoone onto function.
(Contributed by Mario Carneiro, 12Jan2013.)



Theorem  f1oprg 5168 
An unordered pair of ordered pairs with different elements is a onetoone
onto function. (Contributed by Alexander van der Vekens, 14Aug2017.)



Theorem  tz6.122 5169* 
Function value when
is not a function. Theorem 6.12(2) of
[TakeutiZaring] p. 27.
(Contributed by NM, 30Apr2004.) (Proof
shortened by Mario Carneiro, 31Aug2015.)



Theorem  fveu 5170* 
The value of a function at a unique point. (Contributed by Scott
Fenton, 6Oct2017.)



Theorem  brprcneu 5171* 
If is a proper class,
then there is no unique binary relationship
with as the
first element. (Contributed by Scott Fenton,
7Oct2017.)



Theorem  fvprc 5172 
A function's value at a proper class is the empty set. (Contributed by
NM, 20May1998.)



Theorem  fv2 5173* 
Alternate definition of function value. Definition 10.11 of [Quine]
p. 68. (Contributed by NM, 30Apr2004.) (Proof shortened by Andrew
Salmon, 17Sep2011.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  dffv3g 5174* 
A definition of function value in terms of iota. (Contributed by Jim
Kingdon, 29Dec2018.)



Theorem  dffv4g 5175* 
The previous definition of function value, from before the
operator was introduced. Although based on the idea embodied by
Definition 10.2 of [Quine] p. 65 (see args 4694), this definition
apparently does not appear in the literature. (Contributed by NM,
1Aug1994.)



Theorem  elfv 5176* 
Membership in a function value. (Contributed by NM, 30Apr2004.)



Theorem  fveq1 5177 
Equality theorem for function value. (Contributed by NM,
29Dec1996.)



Theorem  fveq2 5178 
Equality theorem for function value. (Contributed by NM,
29Dec1996.)



Theorem  fveq1i 5179 
Equality inference for function value. (Contributed by NM,
2Sep2003.)



Theorem  fveq1d 5180 
Equality deduction for function value. (Contributed by NM,
2Sep2003.)



Theorem  fveq2i 5181 
Equality inference for function value. (Contributed by NM,
28Jul1999.)



Theorem  fveq2d 5182 
Equality deduction for function value. (Contributed by NM,
29May1999.)



Theorem  fveq12i 5183 
Equality deduction for function value. (Contributed by FL,
27Jun2014.)



Theorem  fveq12d 5184 
Equality deduction for function value. (Contributed by FL,
22Dec2008.)



Theorem  nffv 5185 
Boundvariable hypothesis builder for function value. (Contributed by
NM, 14Nov1995.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  nffvmpt1 5186* 
Boundvariable hypothesis builder for mapping, special case.
(Contributed by Mario Carneiro, 25Dec2016.)



Theorem  nffvd 5187 
Deduction version of boundvariable hypothesis builder nffv 5185.
(Contributed by NM, 10Nov2005.) (Revised by Mario Carneiro,
15Oct2016.)



Theorem  funfveu 5188* 
A function has one value given an argument in its domain. (Contributed
by Jim Kingdon, 29Dec2018.)



Theorem  fvss 5189* 
The value of a function is a subset of if every element that could
be a candidate for the value is a subset of . (Contributed by
Mario Carneiro, 24May2019.)



Theorem  fvssunirng 5190 
The result of a function value is always a subset of the union of the
range, if the input is a set. (Contributed by Stefan O'Rear,
2Nov2014.) (Revised by Mario Carneiro, 24May2019.)



Theorem  relfvssunirn 5191 
The result of a function value is always a subset of the union of the
range, even if it is invalid and thus empty. (Contributed by Stefan
O'Rear, 2Nov2014.) (Revised by Mario Carneiro, 24May2019.)



Theorem  funfvex 5192 
The value of a function exists. A special case of Corollary 6.13 of
[TakeutiZaring] p. 27.
(Contributed by Jim Kingdon, 29Dec2018.)



Theorem  relrnfvex 5193 
If a function has a set range, then the function value exists
unconditional on the domain. (Contributed by Mario Carneiro,
24May2019.)



Theorem  fvexg 5194 
Evaluating a set function at a set exists. (Contributed by Mario
Carneiro and Jim Kingdon, 28May2019.)



Theorem  fvex 5195 
Evaluating a set function at a set exists. (Contributed by Mario
Carneiro and Jim Kingdon, 28May2019.)



Theorem  sefvex 5196 
If a function is setlike, then the function value exists if the input
does. (Contributed by Mario Carneiro, 24May2019.)

Se


Theorem  fv3 5197* 
Alternate definition of the value of a function. Definition 6.11 of
[TakeutiZaring] p. 26.
(Contributed by NM, 30Apr2004.) (Revised by
Mario Carneiro, 31Aug2015.)



Theorem  fvres 5198 
The value of a restricted function. (Contributed by NM, 2Aug1994.)



Theorem  funssfv 5199 
The value of a member of the domain of a subclass of a function.
(Contributed by NM, 15Aug1994.)



Theorem  tz6.121 5200* 
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed
by NM, 30Apr2004.)

