Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  elrnrexdm 5334* 
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 5335* 
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 5336* 
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 5337* 
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20Aug2015.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  fmptco 5358* 
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 5359* 
Version of fmptco 5358 where needn't be distinct from .
(Contributed by NM, 27Dec2014.)



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



Theorem  fcompt 5361* 
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 5362 
Composition with a constant function. (Contributed by Stefan O'Rear,
11Mar2015.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  fmptsn 5380* 
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 5381* 
Append an additional value to a function. (Contributed by NM,
6Jun2006.) (Revised by Mario Carneiro, 31Aug2015.)



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



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



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



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



Theorem  fvsn 5386 
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 12Aug1994.)



Theorem  fvsng 5387 
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 26Oct2012.)



Theorem  fvsnun1 5388 
The value of a function with one of its ordered pairs replaced, at the
replaced ordered pair. See also fvsnun2 5389. (Contributed by NM,
23Sep2007.)



Theorem  fvsnun2 5389 
The value of a function with one of its ordered pairs replaced, at
arguments other than the replaced one. See also fvsnun1 5388.
(Contributed by NM, 23Sep2007.)



Theorem  fsnunf 5390 
Adjoining a point to a function gives a function. (Contributed by Stefan
O'Rear, 28Feb2015.)



Theorem  fsnunfv 5391 
Recover the added point from a pointadded function. (Contributed by
Stefan O'Rear, 28Feb2015.) (Revised by NM, 18May2017.)



Theorem  fsnunres 5392 
Recover the original function from a pointadded function. (Contributed
by Stefan O'Rear, 28Feb2015.)



Theorem  fvpr1 5393 
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20Jun2010.)



Theorem  fvpr2 5394 
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20Jun2010.)



Theorem  fvpr1g 5395 
The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3Dec2017.)



Theorem  fvpr2g 5396 
The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3Dec2017.)



Theorem  fvtp1g 5397 
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4Dec2017.)



Theorem  fvtp2g 5398 
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4Dec2017.)



Theorem  fvtp3g 5399 
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4Dec2017.)



Theorem  fvtp1 5400 
The first value of a function with a domain of three elements.
(Contributed by NM, 14Sep2011.)

