Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dfmpt3 5021 
Alternate definition for the "maps to" notation dfmpt 3820. (Contributed
by Mario Carneiro, 30Dec2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  fex2 5059 
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 5060 
Two ways of specifying a partial function from to .
(Contributed by NM, 13Nov2007.)



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



Theorem  opelf 5062 
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 5063 
The union of two functions with disjoint domains. (Contributed by NM,
22Sep2004.)



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



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



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



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



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



Theorem  resasplitss 5069 
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 5070 
Composition of a mapping and restricted identity. (Contributed by NM,
13Dec2003.) (Proof shortened by Andrew Salmon, 17Sep2011.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  f1fn 5093 
A onetoone mapping is a function on its domain. (Contributed by NM,
8Mar2014.)



Theorem  f1fun 5094 
A onetoone mapping is a function. (Contributed by NM, 8Mar2014.)



Theorem  f1rel 5095 
A onetoone onto mapping is a relation. (Contributed by NM,
8Mar2014.)



Theorem  f1dm 5096 
The domain of a onetoone mapping. (Contributed by NM, 8Mar2014.)



Theorem  f1ss 5097 
A function that is onetoone is also onetoone on some superset of its
range. (Contributed by Mario Carneiro, 12Jan2013.)



Theorem  f1ssr 5098 
Combine a onetoone function with a restriction on the domain.
(Contributed by Stefan O'Rear, 20Feb2015.)



Theorem  f1ssres 5099 
A function that is onetoone is also onetoone on some aubset of its
domain. (Contributed by Mario Carneiro, 17Jan2015.)



Theorem  f1cnvcnv 5100 
Two ways to express that a set (not necessarily a function) is
onetoone. Each side is equivalent to Definition 6.4(3) of
[TakeutiZaring] p. 24, who use the
notation "Un_{2} (A)" for onetoone.
We
do not introduce a separate notation since we rarely use it. (Contributed
by NM, 13Aug2004.)

