Type  Label  Description 
Statement 

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



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



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



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



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



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



Theorem  fvmptd3 5507* 
Deduction version of fvmpt 5491. (Contributed by Glauco Siliprandi,
23Oct2021.)



Theorem  elfvmptrab1 5508* 
Implications for the value of a function defined by the mapsto notation
with a class abstraction as a result having an element. Here, the base
set of the class abstraction depends on the argument of the function.
(Contributed by Alexander van der Vekens, 15Jul2018.)



Theorem  elfvmptrab 5509* 
Implications for the value of a function defined by the mapsto notation
with a class abstraction as a result having an element. (Contributed by
Alexander van der Vekens, 15Jul2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  elrnrexdm 5552* 
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 5553* 
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 5554* 
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 5555* 
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20Aug2015.)



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



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



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



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



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



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



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



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



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



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



Theorem  fvmptelrn 5566* 
The value of a function at a point of its domain belongs to its
codomain. (Contributed by Glauco Siliprandi, 26Jun2021.)



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



Theorem  fmpttd 5568* 
Version of fmptd 5567 with inlined definition. Domain and codomain
of the
mapping operation; deduction form. (Contributed by Glauco Siliprandi,
23Oct2021.) (Proof shortened by BJ, 16Aug2022.)



Theorem  fmpt3d 5569* 
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4Jun2017.)



Theorem  fmptdf 5570* 
A version of fmptd 5567 using boundvariable hypothesis instead of a
distinct variable condition for . (Contributed by Glauco
Siliprandi, 29Jun2017.)



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



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



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



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



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



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



Theorem  resflem 5577* 
A lemma to bound the range of a restriction. The conclusion would also
hold with in place of (provided
does not
occur in ). If
that stronger result is needed, it is however
simpler to use the instance of resflem 5577 where
is
substituted for (in both the conclusion and the third hypothesis).
(Contributed by BJ, 4Jul2022.)



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



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



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



Theorem  cofmpt 5582* 
Express composition of a mapsto function with another function in a
mapsto notation. (Contributed by Thierry Arnoux, 29Jun2017.)



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



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



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



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



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



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



Theorem  dfmpt 5590 
Alternate definition for the mapsto notation dfmpt 3986 (although it
requires that
be a set). (Contributed by NM, 24Aug2010.)
(Revised by Mario Carneiro, 30Dec2016.)



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



Theorem  dfmptg 5592 
Alternate definition for the mapsto notation dfmpt 3986 (which requires
that be a set).
(Contributed by Jim Kingdon, 9Jan2019.)



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



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



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



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



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



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



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



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

