Type  Label  Description 
Statement 

Theorem  fndmu 5101 
A function has a unique domain. (Contributed by NM, 11Aug1994.)



Theorem  fnbr 5102 
The first argument of binary relation on a function belongs to the
function's domain. (Contributed by NM, 7May2004.)



Theorem  fnop 5103 
The first argument of an ordered pair in a function belongs to the
function's domain. (Contributed by NM, 8Aug1994.)



Theorem  fneu 5104* 
There is exactly one value of a function. (Contributed by NM,
22Apr2004.) (Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fneu2 5105* 
There is exactly one value of a function. (Contributed by NM,
7Nov1995.)



Theorem  fnun 5106 
The union of two functions with disjoint domains. (Contributed by NM,
22Sep2004.)



Theorem  fnunsn 5107 
Extension of a function with a new ordered pair. (Contributed by NM,
28Sep2013.) (Revised by Mario Carneiro, 30Apr2015.)



Theorem  fnco 5108 
Composition of two functions. (Contributed by NM, 22May2006.)



Theorem  fnresdm 5109 
A function does not change when restricted to its domain. (Contributed by
NM, 5Sep2004.)



Theorem  fnresdisj 5110 
A function restricted to a class disjoint with its domain is empty.
(Contributed by NM, 23Sep2004.)



Theorem  2elresin 5111 
Membership in two functions restricted by each other's domain.
(Contributed by NM, 8Aug1994.)



Theorem  fnssresb 5112 
Restriction of a function with a subclass of its domain. (Contributed by
NM, 10Oct2007.)



Theorem  fnssres 5113 
Restriction of a function with a subclass of its domain. (Contributed by
NM, 2Aug1994.)



Theorem  fnresin1 5114 
Restriction of a function's domain with an intersection. (Contributed by
NM, 9Aug1994.)



Theorem  fnresin2 5115 
Restriction of a function's domain with an intersection. (Contributed by
NM, 9Aug1994.)



Theorem  fnres 5116* 
An equivalence for functionality of a restriction. Compare dffun8 5029.
(Contributed by Mario Carneiro, 20May2015.)



Theorem  fnresi 5117 
Functionality and domain of restricted identity. (Contributed by NM,
27Aug2004.)



Theorem  fnima 5118 
The image of a function's domain is its range. (Contributed by NM,
4Nov2004.) (Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fn0 5119 
A function with empty domain is empty. (Contributed by NM, 15Apr1998.)
(Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fnimadisj 5120 
A class that is disjoint with the domain of a function has an empty image
under the function. (Contributed by FL, 24Jan2007.)



Theorem  fnimaeq0 5121 
Images under a function never map nonempty sets to empty sets.
(Contributed by Stefan O'Rear, 21Jan2015.)



Theorem  dfmpt3 5122 
Alternate definition for the mapsto notation dfmpt 3893. (Contributed
by Mario Carneiro, 30Dec2016.)



Theorem  fnopabg 5123* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by NM, 30Jan2004.) (Proof shortened by Mario Carneiro,
4Dec2016.)



Theorem  fnopab 5124* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by NM, 5Mar1996.)



Theorem  mptfng 5125* 
The mapsto notation defines a function with domain. (Contributed by
Scott Fenton, 21Mar2011.)



Theorem  fnmpt 5126* 
The mapsto notation defines a function with domain. (Contributed by
NM, 9Apr2013.)



Theorem  mpt0 5127 
A mapping operation with empty domain. (Contributed by Mario Carneiro,
28Dec2014.)



Theorem  fnmpti 5128* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by NM, 29Jan2004.) (Revised by Mario Carneiro,
31Aug2015.)



Theorem  dmmpti 5129* 
Domain of an orderedpair class abstraction that specifies a function.
(Contributed by NM, 6Sep2005.) (Revised by Mario Carneiro,
31Aug2015.)



Theorem  mptun 5130 
Union of mappings which are mutually compatible. (Contributed by Mario
Carneiro, 31Aug2015.)



Theorem  feq1 5131 
Equality theorem for functions. (Contributed by NM, 1Aug1994.)



Theorem  feq2 5132 
Equality theorem for functions. (Contributed by NM, 1Aug1994.)



Theorem  feq3 5133 
Equality theorem for functions. (Contributed by NM, 1Aug1994.)



Theorem  feq23 5134 
Equality theorem for functions. (Contributed by FL, 14Jul2007.) (Proof
shortened by Andrew Salmon, 17Sep2011.)



Theorem  feq1d 5135 
Equality deduction for functions. (Contributed by NM, 19Feb2008.)



Theorem  feq2d 5136 
Equality deduction for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq12d 5137 
Equality deduction for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq123d 5138 
Equality deduction for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq123 5139 
Equality theorem for functions. (Contributed by FL, 16Nov2008.)



Theorem  feq1i 5140 
Equality inference for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq2i 5141 
Equality inference for functions. (Contributed by NM, 5Sep2011.)



Theorem  feq23i 5142 
Equality inference for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq23d 5143 
Equality deduction for functions. (Contributed by NM, 8Jun2013.)



Theorem  nff 5144 
Boundvariable hypothesis builder for a mapping. (Contributed by NM,
29Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  sbcfng 5145* 
Distribute proper substitution through the function predicate with a
domain. (Contributed by Alexander van der Vekens, 15Jul2018.)



Theorem  sbcfg 5146* 
Distribute proper substitution through the function predicate with
domain and codomain. (Contributed by Alexander van der Vekens,
15Jul2018.)



Theorem  ffn 5147 
A mapping is a function. (Contributed by NM, 2Aug1994.)



Theorem  ffnd 5148 
A mapping is a function with domain, deduction form. (Contributed by
Glauco Siliprandi, 17Aug2020.)



Theorem  dffn2 5149 
Any function is a mapping into . (Contributed by NM, 31Oct1995.)
(Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  ffun 5150 
A mapping is a function. (Contributed by NM, 3Aug1994.)



Theorem  frel 5151 
A mapping is a relation. (Contributed by NM, 3Aug1994.)



Theorem  fdm 5152 
The domain of a mapping. (Contributed by NM, 2Aug1994.)



Theorem  fdmd 5153 
Deduction form of fdm 5152. The domain of a mapping. (Contributed by
Glauco Siliprandi, 26Jun2021.)



Theorem  fdmi 5154 
The domain of a mapping. (Contributed by NM, 28Jul2008.)



Theorem  frn 5155 
The range of a mapping. (Contributed by NM, 3Aug1994.)



Theorem  dffn3 5156 
A function maps to its range. (Contributed by NM, 1Sep1999.)



Theorem  fss 5157 
Expanding the codomain of a mapping. (Contributed by NM, 10May1998.)
(Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fssd 5158 
Expanding the codomain of a mapping, deduction form. (Contributed by
Glauco Siliprandi, 11Dec2019.)



Theorem  fssdmd 5159 
Expressing that a class is a subclass of the domain of a function
expressed in mapsto notation, deduction form. (Contributed by AV,
21Aug2022.)



Theorem  fssdm 5160 
Expressing that a class is a subclass of the domain of a function
expressed in mapsto notation, semideduction form. (Contributed by AV,
21Aug2022.)



Theorem  fco 5161 
Composition of two mappings. (Contributed by NM, 29Aug1999.) (Proof
shortened by Andrew Salmon, 17Sep2011.)



Theorem  fco2 5162 
Functionality of a composition with weakened out of domain condition on
the first argument. (Contributed by Stefan O'Rear, 11Mar2015.)



Theorem  fssxp 5163 
A mapping is a class of ordered pairs. (Contributed by NM, 3Aug1994.)
(Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fex2 5164 
A function with bounded domain and range is a set. This version is proven
without the Axiom of Replacement. (Contributed by Mario Carneiro,
24Jun2015.)



Theorem  funssxp 5165 
Two ways of specifying a partial function from to .
(Contributed by NM, 13Nov2007.)



Theorem  ffdm 5166 
A mapping is a partial function. (Contributed by NM, 25Nov2007.)



Theorem  opelf 5167 
The members of an ordered pair element of a mapping belong to the
mapping's domain and codomain. (Contributed by NM, 10Dec2003.)
(Revised by Mario Carneiro, 26Apr2015.)



Theorem  fun 5168 
The union of two functions with disjoint domains. (Contributed by NM,
22Sep2004.)



Theorem  fun2 5169 
The union of two functions with disjoint domains. (Contributed by Mario
Carneiro, 12Mar2015.)



Theorem  fnfco 5170 
Composition of two functions. (Contributed by NM, 22May2006.)



Theorem  fssres 5171 
Restriction of a function with a subclass of its domain. (Contributed by
NM, 23Sep2004.)



Theorem  fssres2 5172 
Restriction of a restricted function with a subclass of its domain.
(Contributed by NM, 21Jul2005.)



Theorem  fresin 5173 
An identity for the mapping relationship under restriction. (Contributed
by Scott Fenton, 4Sep2011.) (Proof shortened by Mario Carneiro,
26May2016.)



Theorem  resasplitss 5174 
If two functions agree on their common domain, their union contains a
union of three functions with pairwise disjoint domains. If we assumed
the law of the excluded middle, this would be equality rather than subset.
(Contributed by Jim Kingdon, 28Dec2018.)



Theorem  fcoi1 5175 
Composition of a mapping and restricted identity. (Contributed by NM,
13Dec2003.) (Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fcoi2 5176 
Composition of restricted identity and a mapping. (Contributed by NM,
13Dec2003.) (Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  feu 5177* 
There is exactly one value of a function in its codomain. (Contributed
by NM, 10Dec2003.)



Theorem  fcnvres 5178 
The converse of a restriction of a function. (Contributed by NM,
26Mar1998.)



Theorem  fimacnvdisj 5179 
The preimage of a class disjoint with a mapping's codomain is empty.
(Contributed by FL, 24Jan2007.)



Theorem  fintm 5180* 
Function into an intersection. (Contributed by Jim Kingdon,
28Dec2018.)



Theorem  fin 5181 
Mapping into an intersection. (Contributed by NM, 14Sep1999.) (Proof
shortened by Andrew Salmon, 17Sep2011.)



Theorem  fabexg 5182* 
Existence of a set of functions. (Contributed by Paul Chapman,
25Feb2008.)



Theorem  fabex 5183* 
Existence of a set of functions. (Contributed by NM, 3Dec2007.)



Theorem  dmfex 5184 
If a mapping is a set, its domain is a set. (Contributed by NM,
27Aug2006.) (Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  f0 5185 
The empty function. (Contributed by NM, 14Aug1999.)



Theorem  f00 5186 
A class is a function with empty codomain iff it and its domain are empty.
(Contributed by NM, 10Dec2003.)



Theorem  f0bi 5187 
A function with empty domain is empty. (Contributed by Alexander van der
Vekens, 30Jun2018.)



Theorem  f0dom0 5188 
A function is empty iff it has an empty domain. (Contributed by AV,
10Feb2019.)



Theorem  f0rn0 5189* 
If there is no element in the range of a function, its domain must be
empty. (Contributed by Alexander van der Vekens, 12Jul2018.)



Theorem  fconst 5190 
A cross product with a singleton is a constant function. (Contributed
by NM, 14Aug1999.) (Proof shortened by Andrew Salmon,
17Sep2011.)



Theorem  fconstg 5191 
A cross product with a singleton is a constant function. (Contributed
by NM, 19Oct2004.)



Theorem  fnconstg 5192 
A cross product with a singleton is a constant function. (Contributed by
NM, 24Jul2014.)



Theorem  fconst6g 5193 
Constant function with loose range. (Contributed by Stefan O'Rear,
1Feb2015.)



Theorem  fconst6 5194 
A constant function as a mapping. (Contributed by Jeff Madsen,
30Nov2009.) (Revised by Mario Carneiro, 22Apr2015.)



Theorem  f1eq1 5195 
Equality theorem for onetoone functions. (Contributed by NM,
10Feb1997.)



Theorem  f1eq2 5196 
Equality theorem for onetoone functions. (Contributed by NM,
10Feb1997.)



Theorem  f1eq3 5197 
Equality theorem for onetoone functions. (Contributed by NM,
10Feb1997.)



Theorem  nff1 5198 
Boundvariable hypothesis builder for a onetoone function.
(Contributed by NM, 16May2004.)



Theorem  dff12 5199* 
Alternate definition of a onetoone function. (Contributed by NM,
31Dec1996.)



Theorem  f1f 5200 
A onetoone mapping is a mapping. (Contributed by NM, 31Dec1996.)

