Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  elrnrexdm 5249* 
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 5250* 
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 5251* 
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 5252* 
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20Aug2015.)



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



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



Theorem  dff3im 5255* 
Property of a mapping. (Contributed by Jim Kingdon, 4Jan2019.)



Theorem  dff4im 5256* 
Property of a mapping. (Contributed by Jim Kingdon, 4Jan2019.)



Theorem  dffo3 5257* 
An onto mapping expressed in terms of function values. (Contributed by
NM, 29Oct2006.)



Theorem  dffo4 5258* 
Alternate definition of an onto mapping. (Contributed by NM,
20Mar2007.)



Theorem  dffo5 5259* 
Alternate definition of an onto mapping. (Contributed by NM,
20Mar2007.)



Theorem  foelrn 5260* 
Property of a surjective function. (Contributed by Jeff Madsen,
4Jan2011.)



Theorem  foco2 5261 
If a composition of two functions is surjective, then the function on
the left is surjective. (Contributed by Jeff Madsen, 16Jun2011.)



Theorem  fmpt 5262* 
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26Jul2013.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  f1ompt 5263* 
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30May2015.) (Revised by Mario Carneiro, 4Dec2016.)



Theorem  fmpti 5264* 
Functionality of the mapping operation. (Contributed by NM,
19Mar2005.) (Revised by Mario Carneiro, 1Sep2015.)



Theorem  fmptd 5265* 
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13Jan2013.)



Theorem  ffnfv 5266* 
A function maps to a class to which all values belong. (Contributed by
NM, 3Dec2003.)



Theorem  ffnfvf 5267 
A function maps to a class to which all values belong. This version of
ffnfv 5266 uses boundvariable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28Sep2006.)



Theorem  fnfvrnss 5268* 
An upper bound for range determined by function values. (Contributed by
NM, 8Oct2004.)



Theorem  rnmptss 5269* 
The range of an operation given by the "maps to" notation as a
subset.
(Contributed by Thierry Arnoux, 24Sep2017.)



Theorem  fmpt2d 5270* 
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27Dec2014.)



Theorem  ffvresb 5271* 
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14Nov2013.)



Theorem  f1oresrab 5272* 
Build a bijection between restricted abstract builders, given a
bijection between the base classes, deduction version. (Contributed by
Thierry Arnoux, 17Aug2018.)



Theorem  fmptco 5273* 
Composition of two functions expressed as orderedpair class
abstractions. If has the equation ( x + 2 ) and the
equation ( 3 * z ) then has the equation ( 3 * ( x +
2 ) ) . (Contributed by FL, 21Jun2012.) (Revised by Mario Carneiro,
24Jul2014.)



Theorem  fmptcof 5274* 
Version of fmptco 5273 where needn't be distinct from .
(Contributed by NM, 27Dec2014.)



Theorem  fmptcos 5275* 
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22May2006.) (Revised by Mario Carneiro,
31Aug2015.)



Theorem  fcompt 5276* 
Express composition of two functions as a mapsto applying both in
sequence. (Contributed by Stefan O'Rear, 5Oct2014.) (Proof shortened
by Mario Carneiro, 27Dec2014.)



Theorem  fcoconst 5277 
Composition with a constant function. (Contributed by Stefan O'Rear,
11Mar2015.)



Theorem  fsn 5278 
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 10Dec2003.)



Theorem  fsng 5279 
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 26Oct2012.)



Theorem  fsn2 5280 
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by NM, 19May2004.)



Theorem  xpsng 5281 
The cross product of two singletons. (Contributed by Mario Carneiro,
30Apr2015.)



Theorem  xpsn 5282 
The cross product of two singletons. (Contributed by NM,
4Nov2006.)



Theorem  dfmpt 5283 
Alternate definition for the "maps to" notation dfmpt 3811 (although it
requires that
be a set). (Contributed by NM, 24Aug2010.)
(Revised by Mario Carneiro, 30Dec2016.)



Theorem  fnasrn 5284 
A function expressed as the range of another function. (Contributed by
Mario Carneiro, 22Jun2013.) (Proof shortened by Mario Carneiro,
31Aug2015.)



Theorem  dfmptg 5285 
Alternate definition for the "maps to" notation dfmpt 3811 (which requires
that be a
set). (Contributed by Jim Kingdon, 9Jan2019.)



Theorem  fnasrng 5286 
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9Jan2019.)



Theorem  ressnop0 5287 
If is not in , then the restriction of a
singleton of
to is
null. (Contributed by Scott Fenton,
15Apr2011.)



Theorem  fpr 5288 
A function with a domain of two elements. (Contributed by Jeff Madsen,
20Jun2010.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  fprg 5289 
A function with a domain of two elements. (Contributed by FL,
2Feb2014.)



Theorem  ftpg 5290 
A function with a domain of three elements. (Contributed by Alexander van
der Vekens, 4Dec2017.)



Theorem  ftp 5291 
A function with a domain of three elements. (Contributed by Stefan
O'Rear, 17Oct2014.) (Proof shortened by Alexander van der Vekens,
23Jan2018.)



Theorem  fnressn 5292 
A function restricted to a singleton. (Contributed by NM,
9Oct2004.)



Theorem  fressnfv 5293 
The value of a function restricted to a singleton. (Contributed by NM,
9Oct2004.)



Theorem  fvconst 5294 
The value of a constant function. (Contributed by NM, 30May1999.)



Theorem  fmptsn 5295* 
Express a singleton function in mapsto notation. (Contributed by NM,
6Jun2006.) (Proof shortened by Andrew Salmon, 22Oct2011.) (Revised
by Stefan O'Rear, 28Feb2015.)



Theorem  fmptap 5296* 
Append an additional value to a function. (Contributed by NM,
6Jun2006.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  fmptapd 5297* 
Append an additional value to a function. (Contributed by Thierry
Arnoux, 3Jan2017.)



Theorem  fmptpr 5298* 
Express a pair function in mapsto notation. (Contributed by Thierry
Arnoux, 3Jan2017.)



Theorem  fvresi 5299 
The value of a restricted identity function. (Contributed by NM,
19May2004.)



Theorem  fvunsng 5300 
Remove an ordered pair not participating in a function value.
(Contributed by Jim Kingdon, 7Jan2019.)

