Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



Theorem  tz6.122 5112* 
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 5113* 
The value of a function at a unique point. (Contributed by Scott
Fenton, 6Oct2017.)



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



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



Theorem  fv2 5116* 
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 5117* 
A definition of function value in terms of iota. (Contributed by Jim
Kingdon, 29Dec2018.)



Theorem  dffv4g 5118* 
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 4637), this definition
apparently does not appear in the literature. (Contributed by NM,
1Aug1994.)



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  fvss 5132* 
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 5133 
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 5134 
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 5135 
The value of a function exists. A special case of Corollary 6.13 of
[TakeutiZaring] p. 27.
(Contributed by Jim Kingdon, 29Dec2018.)



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



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



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



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

Se 

Theorem  fv3 5140* 
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 5141 
The value of a restricted function. (Contributed by NM, 2Aug1994.)



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



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



Theorem  tz6.12 5144* 
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed
by NM, 10Jul1994.)



Theorem  tz6.12f 5145* 
Function value, using boundvariable hypotheses instead of distinct
variable conditions. (Contributed by NM, 30Aug1999.)



Theorem  tz6.12c 5146* 
Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by
NM, 30Apr2004.)



Theorem  ndmfvg 5147 
The value of a class outside its domain is the empty set. (Contributed
by Jim Kingdon, 15Jan2019.)



Theorem  relelfvdm 5148 
If a function value has a member, the argument belongs to the domain.
(Contributed by Jim Kingdon, 22Jan2019.)



Theorem  nfvres 5149 
The value of a nonmember of a restriction is the empty set.
(Contributed by NM, 13Nov1995.)



Theorem  nfunsn 5150 
If the restriction of a class to a singleton is not a function, its
value is the empty set. (Contributed by NM, 8Aug2010.) (Proof
shortened by Andrew Salmon, 22Oct2011.)



Theorem  0fv 5151 
Function value of the empty set. (Contributed by Stefan O'Rear,
26Nov2014.)



Theorem  csbfv12g 5152 
Move class substitution in and out of a function value. (Contributed by
NM, 11Nov2005.)



Theorem  csbfv2g 5153* 
Move class substitution in and out of a function value. (Contributed by
NM, 10Nov2005.)



Theorem  csbfvg 5154* 
Substitution for a function value. (Contributed by NM, 1Jan2006.)



Theorem  funbrfv 5155 
The second argument of a binary relation on a function is the function's
value. (Contributed by NM, 30Apr2004.) (Revised by Mario Carneiro,
28Apr2015.)



Theorem  funopfv 5156 
The second element in an ordered pair member of a function is the
function's value. (Contributed by NM, 19Jul1996.)



Theorem  fnbrfvb 5157 
Equivalence of function value and binary relation. (Contributed by NM,
19Apr2004.) (Revised by Mario Carneiro, 28Apr2015.)



Theorem  fnopfvb 5158 
Equivalence of function value and ordered pair membership. (Contributed
by NM, 7Nov1995.)



Theorem  funbrfvb 5159 
Equivalence of function value and binary relation. (Contributed by NM,
26Mar2006.)



Theorem  funopfvb 5160 
Equivalence of function value and ordered pair membership. Theorem
4.3(ii) of [Monk1] p. 42. (Contributed by
NM, 26Jan1997.)



Theorem  funbrfv2b 5161 
Function value in terms of a binary relation. (Contributed by Mario
Carneiro, 19Mar2014.)



Theorem  dffn5im 5162* 
Representation of a function in terms of its values. The converse holds
given the law of the excluded middle; as it is we have most of the
converse via funmpt 4881 and dmmptss 4760. (Contributed by Jim Kingdon,
31Dec2018.)



Theorem  fnrnfv 5163* 
The range of a function expressed as a collection of the function's
values. (Contributed by NM, 20Oct2005.) (Proof shortened by Mario
Carneiro, 31Aug2015.)



Theorem  fvelrnb 5164* 
A member of a function's range is a value of the function. (Contributed
by NM, 31Oct1995.)



Theorem  dfimafn 5165* 
Alternate definition of the image of a function. (Contributed by Raph
Levien, 20Nov2006.)



Theorem  dfimafn2 5166* 
Alternate definition of the image of a function as an indexed union of
singletons of function values. (Contributed by Raph Levien,
20Nov2006.)



Theorem  funimass4 5167* 
Membership relation for the values of a function whose image is a
subclass. (Contributed by Raph Levien, 20Nov2006.)



Theorem  fvelima 5168* 
Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42.
(Contributed by NM, 29Apr2004.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  feqmptd 5169* 
Deduction form of dffn5im 5162. (Contributed by Mario Carneiro,
8Jan2015.)



Theorem  feqresmpt 5170* 
Express a restricted function as a mapping. (Contributed by Mario
Carneiro, 18May2016.)



Theorem  dffn5imf 5171* 
Representation of a function in terms of its values. (Contributed by
Jim Kingdon, 31Dec2018.)



Theorem  fvelimab 5172* 
Function value in an image. (Contributed by NM, 20Jan2007.) (Proof
shortened by Andrew Salmon, 22Oct2011.) (Revised by David Abernethy,
17Dec2011.)



Theorem  fvi 5173 
The value of the identity function. (Contributed by NM, 1May2004.)
(Revised by Mario Carneiro, 28Apr2015.)



Theorem  fniinfv 5174* 
The indexed intersection of a function's values is the intersection of
its range. (Contributed by NM, 20Oct2005.)



Theorem  fnsnfv 5175 
Singleton of function value. (Contributed by NM, 22May1998.)



Theorem  fnimapr 5176 
The image of a pair under a function. (Contributed by Jeff Madsen,
6Jan2011.)



Theorem  ssimaex 5177* 
The existence of a subimage. (Contributed by NM, 8Apr2007.)



Theorem  ssimaexg 5178* 
The existence of a subimage. (Contributed by FL, 15Apr2007.)



Theorem  funfvdm 5179 
A simplified expression for the value of a function when we know it's a
function. (Contributed by Jim Kingdon, 1Jan2019.)



Theorem  funfvdm2 5180* 
The value of a function. Definition of function value in [Enderton]
p. 43. (Contributed by Jim Kingdon, 1Jan2019.)



Theorem  funfvdm2f 5181 
The value of a function. Version of funfvdm2 5180 using a boundvariable
hypotheses instead of distinct variable conditions. (Contributed by Jim
Kingdon, 1Jan2019.)



Theorem  fvun1 5182 
The value of a union when the argument is in the first domain.
(Contributed by Scott Fenton, 29Jun2013.)



Theorem  fvun2 5183 
The value of a union when the argument is in the second domain.
(Contributed by Scott Fenton, 29Jun2013.)



Theorem  dmfco 5184 
Domains of a function composition. (Contributed by NM, 27Jan1997.)



Theorem  fvco2 5185 
Value of a function composition. Similar to second part of Theorem 3H
of [Enderton] p. 47. (Contributed by
NM, 9Oct2004.) (Proof shortened
by Andrew Salmon, 22Oct2011.) (Revised by Stefan O'Rear,
16Oct2014.)



Theorem  fvco 5186 
Value of a function composition. Similar to Exercise 5 of [TakeutiZaring]
p. 28. (Contributed by NM, 22Apr2006.) (Proof shortened by Mario
Carneiro, 26Dec2014.)



Theorem  fvco3 5187 
Value of a function composition. (Contributed by NM, 3Jan2004.)
(Revised by Mario Carneiro, 26Dec2014.)



Theorem  fvopab3g 5188* 
Value of a function given by orderedpair class abstraction.
(Contributed by NM, 6Mar1996.) (Revised by Mario Carneiro,
28Apr2015.)



Theorem  fvopab3ig 5189* 
Value of a function given by orderedpair class abstraction.
(Contributed by NM, 23Oct1999.)



Theorem  fvmptss2 5190* 
A mapping always evaluates to a subset of the substituted expression in
the mapping, even if this is a proper class, or we are out of the
domain. (Contributed by Mario Carneiro, 13Feb2015.) (Revised by
Mario Carneiro, 3Jul2019.)



Theorem  fvmptg 5191* 
Value of a function given in mapsto notation. (Contributed by NM,
2Oct2007.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  fvmpt 5192* 
Value of a function given in mapsto notation. (Contributed by NM,
17Aug2011.)



Theorem  fvmpts 5193* 
Value of a function given in mapsto notation, using explicit class
substitution. (Contributed by Scott Fenton, 17Jul2013.) (Revised by
Mario Carneiro, 31Aug2015.)



Theorem  fvmpt3 5194* 
Value of a function given in mapsto notation, with a slightly
different sethood condition. (Contributed by Stefan O'Rear,
30Jan2015.)



Theorem  fvmpt3i 5195* 
Value of a function given in mapsto notation, with a slightly different
sethood condition. (Contributed by Mario Carneiro, 11Sep2015.)



Theorem  fvmptd 5196* 
Deduction version of fvmpt 5192. (Contributed by Scott Fenton,
18Feb2013.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  fvmpt2 5197* 
Value of a function given by the "maps to" notation. (Contributed by
FL, 21Jun2010.)



Theorem  fvmptssdm 5198* 
If all the values of the mapping are subsets of a class , then so
is any evaluation of the mapping at a value in the domain of the
mapping. (Contributed by Jim Kingdon, 3Jan2018.)



Theorem  mptfvex 5199* 
Sufficient condition for a mapsto notation to be setlike.
(Contributed by Mario Carneiro, 3Jul2019.)



Theorem  fvmpt2d 5200* 
Deduction version of fvmpt2 5197. (Contributed by Thierry Arnoux,
8Dec2016.)

