Type  Label  Description 
Statement 

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



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



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



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



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



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



Theorem  dffn5im 5307* 
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 5014 and dmmptss 4890. (Contributed by Jim Kingdon,
31Dec2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  fvco4 5333 
Value of a composition. (Contributed by BJ, 7Jul2022.)



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



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



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



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



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



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



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



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



Theorem  fvmpt2 5343* 
Value of a function given by the mapsto notation. (Contributed by FL,
21Jun2010.)



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



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



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



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



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



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



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



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



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



Theorem  eqfnfv 5354* 
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 5355* 
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 5356* 
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2Sep2009.)



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



Theorem  eqfnfv2f 5358* 
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 5354 uses boundvariable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29Jan2004.)



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



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



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



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



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



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



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



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



Theorem  chfnrn 5367* 
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 5368 
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14Oct1996.)



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



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



Theorem  fvimacnv 5371 
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 5054 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20Nov2006.)



Theorem  funimass3 5372 
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 5371 would be the special case of being
a singleton, but it works this way round too." (Contributed by
Raph
Levien, 20Nov2006.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ffvelrni 5390 
A function's value belongs to its codomain. (Contributed by NM,
6Apr2005.)



Theorem  ffvelrnda 5391 
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29Dec2016.)



Theorem  ffvelrnd 5392 
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29Dec2016.)



Theorem  rexrn 5393* 
Restricted existential quantification over the range of a function.
(Contributed by Mario Carneiro, 24Dec2013.) (Revised by Mario
Carneiro, 20Aug2014.)



Theorem  ralrn 5394* 
Restricted universal quantification over the range of a function.
(Contributed by Mario Carneiro, 24Dec2013.) (Revised by Mario
Carneiro, 20Aug2014.)



Theorem  elrnrexdm 5395* 
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 8Dec2017.)



Theorem  elrnrexdmb 5396* 
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 17Dec2017.)



Theorem  eldmrexrn 5397* 
For any element in the domain of a function there is an element in the
range of the function which is the function value for the element of the
domain. (Contributed by Alexander van der Vekens, 8Dec2017.)



Theorem  ralrnmpt 5398* 
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  rexrnmpt 5399* 
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  dff2 5400 
Alternate definition of a mapping. (Contributed by NM, 14Nov2007.)

