Type  Label  Description 
Statement 

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



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



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



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



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



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



Theorem  nfunsn 5207 
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 5208 
Function value of the empty set. (Contributed by Stefan O'Rear,
26Nov2014.)



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



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



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



Theorem  funbrfv 5212 
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 5213 
The second element in an ordered pair member of a function is the
function's value. (Contributed by NM, 19Jul1996.)



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



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



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



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



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



Theorem  dffn5im 5219* 
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 4938 and dmmptss 4817. (Contributed by Jim Kingdon,
31Dec2018.)



Theorem  fnrnfv 5220* 
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 5221* 
A member of a function's range is a value of the function. (Contributed
by NM, 31Oct1995.)



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



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



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



Theorem  fvelima 5225* 
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 5226* 
Deduction form of dffn5im 5219. (Contributed by Mario Carneiro,
8Jan2015.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  fvco2 5242 
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 5243 
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 5244 
Value of a function composition. (Contributed by NM, 3Jan2004.)
(Revised by Mario Carneiro, 26Dec2014.)



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



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



Theorem  fvmptss2 5247* 
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 5248* 
Value of a function given in mapsto notation. (Contributed by NM,
2Oct2007.) (Revised by Mario Carneiro, 31Aug2015.)



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



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



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



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



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



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



Theorem  fvmptssdm 5255* 
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 5256* 
Sufficient condition for a mapsto notation to be setlike.
(Contributed by Mario Carneiro, 3Jul2019.)



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



Theorem  fvmptdf 5258* 
Alternate deduction version of fvmpt 5249, suitable for iteration.
(Contributed by Mario Carneiro, 7Jan2017.)



Theorem  fvmptdv 5259* 
Alternate deduction version of fvmpt 5249, suitable for iteration.
(Contributed by Mario Carneiro, 7Jan2017.)



Theorem  fvmptdv2 5260* 
Alternate deduction version of fvmpt 5249, suitable for iteration.
(Contributed by Mario Carneiro, 7Jan2017.)



Theorem  mpteqb 5261* 
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnfv 5265. (Contributed by Mario Carneiro,
14Nov2014.)



Theorem  fvmptt 5262* 
Closed theorem form of fvmpt 5249. (Contributed by Scott Fenton,
21Feb2013.) (Revised by Mario Carneiro, 11Sep2015.)



Theorem  fvmptf 5263* 
Value of a function given by an orderedpair class abstraction. This
version of fvmptg 5248 uses boundvariable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8Nov2005.) (Revised by
Mario Carneiro, 15Oct2016.)



Theorem  fvopab6 5264* 
Value of a function given by orderedpair class abstraction.
(Contributed by Jeff Madsen, 2Sep2009.) (Revised by Mario Carneiro,
11Sep2015.)



Theorem  eqfnfv 5265* 
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
(Contributed by NM, 3Aug1994.) (Proof shortened by Andrew Salmon,
22Oct2011.) (Proof shortened by Mario Carneiro, 31Aug2015.)



Theorem  eqfnfv2 5266* 
Equality of functions is determined by their values. Exercise 4 of
[TakeutiZaring] p. 28.
(Contributed by NM, 3Aug1994.) (Revised by
Mario Carneiro, 31Aug2015.)



Theorem  eqfnfv3 5267* 
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2Sep2009.)



Theorem  eqfnfvd 5268* 
Deduction for equality of functions. (Contributed by Mario Carneiro,
24Jul2014.)



Theorem  eqfnfv2f 5269* 
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
This version of eqfnfv 5265 uses boundvariable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29Jan2004.)



Theorem  eqfunfv 5270* 
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19Jun2011.)



Theorem  fvreseq 5271* 
Equality of restricted functions is determined by their values.
(Contributed by NM, 3Aug1994.)



Theorem  fndmdif 5272* 
Two ways to express the locus of differences between two functions.
(Contributed by Stefan O'Rear, 17Jan2015.)



Theorem  fndmdifcom 5273 
The difference set between two functions is commutative. (Contributed
by Stefan O'Rear, 17Jan2015.)



Theorem  fndmin 5274* 
Two ways to express the locus of equality between two functions.
(Contributed by Stefan O'Rear, 17Jan2015.)



Theorem  fneqeql 5275 
Two functions are equal iff their equalizer is the whole domain.
(Contributed by Stefan O'Rear, 7Mar2015.)



Theorem  fneqeql2 5276 
Two functions are equal iff their equalizer contains the whole domain.
(Contributed by Stefan O'Rear, 9Mar2015.)



Theorem  fnreseql 5277 
Two functions are equal on a subset iff their equalizer contains that
subset. (Contributed by Stefan O'Rear, 7Mar2015.)



Theorem  chfnrn 5278* 
The range of a choice function (a function that chooses an element from
each member of its domain) is included in the union of its domain.
(Contributed by NM, 31Aug1999.)



Theorem  funfvop 5279 
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14Oct1996.)



Theorem  funfvbrb 5280 
Two ways to say that
is in the domain of .
(Contributed by
Mario Carneiro, 1May2014.)



Theorem  fvimacnvi 5281 
A member of a preimage is a function value argument. (Contributed by NM,
4May2007.)



Theorem  fvimacnv 5282 
The argument of a function value belongs to the preimage of any class
containing the function value. Raph Levien remarks: "This proof is
unsatisfying, because it seems to me that funimass2 4977 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20Nov2006.)



Theorem  funimass3 5283 
A kind of contraposition law that infers an image subclass from a
subclass of a preimage. Raph Levien remarks: "Likely this could
be
proved directly, and fvimacnv 5282 would be the special case of being
a singleton, but it works this way round too." (Contributed by
Raph
Levien, 20Nov2006.)



Theorem  funimass5 5284* 
A subclass of a preimage in terms of function values. (Contributed by
NM, 15May2007.)



Theorem  funconstss 5285* 
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8Mar2007.)



Theorem  elpreima 5286 
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  fniniseg 5287 
Membership in the preimage of a singleton, under a function.
(Contributed by Mario Carneiro, 12May2014.) (Proof shortened by Mario
Carneiro, 28Apr2015.)



Theorem  fncnvima2 5288* 
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1Feb2015.)



Theorem  fniniseg2 5289* 
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1Feb2015.)



Theorem  fnniniseg2 5290* 
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1Feb2015.)



Theorem  rexsupp 5291* 
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23Mar2015.)



Theorem  unpreima 5292 
Preimage of a union. (Contributed by Jeff Madsen, 2Sep2009.)



Theorem  inpreima 5293 
Preimage of an intersection. (Contributed by Jeff Madsen, 2Sep2009.)
(Proof shortened by Mario Carneiro, 14Jun2016.)



Theorem  difpreima 5294 
Preimage of a difference. (Contributed by Mario Carneiro,
14Jun2016.)



Theorem  respreima 5295 
The preimage of a restricted function. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  fimacnv 5296 
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25Jan2007.)



Theorem  fnopfv 5297 
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30Sep2004.)



Theorem  fvelrn 5298 
A function's value belongs to its range. (Contributed by NM,
14Oct1996.)



Theorem  fnfvelrn 5299 
A function's value belongs to its range. (Contributed by NM,
15Oct1996.)



Theorem  ffvelrn 5300 
A function's value belongs to its codomain. (Contributed by NM,
12Aug1999.)

