Type  Label  Description 
Statement 

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



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



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



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



Theorem  frnd 5205 
Deduction form of frn 5204. The range of a mapping. (Contributed by
Glauco Siliprandi, 26Jun2021.)



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



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



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



Theorem  fssdmd 5209 
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 5210 
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 5211 
Composition of two mappings. (Contributed by NM, 29Aug1999.) (Proof
shortened by Andrew Salmon, 17Sep2011.)



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



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



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



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



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



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



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



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



Theorem  fssresd 5222 
Restriction of a function with a subclass of its domain, deduction form.
(Contributed by Glauco Siliprandi, 11Dec2019.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  f0rn0 5240* 
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 5241 
A cross product with a singleton is a constant function. (Contributed
by NM, 14Aug1999.) (Proof shortened by Andrew Salmon,
17Sep2011.)



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



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



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



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



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



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



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



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



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



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



Theorem  f1rn 5252 
The range of a onetoone mapping. (Contributed by BJ, 6Jul2022.)



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



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



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



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



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



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



Theorem  f1ff1 5259 
If a function is onetoone from A to B and is also a function from A to
C, then it is a onetoone function from A to C. (Contributed by BJ,
4Jul2022.)



Theorem  f1ssres 5260 
A function that is onetoone is also onetoone on any subclass of its
domain. (Contributed by Mario Carneiro, 17Jan2015.)



Theorem  f1resf1 5261 
The restriction of an injective function is injective. (Contributed by
AV, 28Jun2022.)



Theorem  f1cnvcnv 5262 
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.)



Theorem  f1co 5263 
Composition of onetoone functions. Exercise 30 of [TakeutiZaring]
p. 25. (Contributed by NM, 28May1998.)



Theorem  foeq1 5264 
Equality theorem for onto functions. (Contributed by NM, 1Aug1994.)



Theorem  foeq2 5265 
Equality theorem for onto functions. (Contributed by NM, 1Aug1994.)



Theorem  foeq3 5266 
Equality theorem for onto functions. (Contributed by NM, 1Aug1994.)



Theorem  nffo 5267 
Boundvariable hypothesis builder for an onto function. (Contributed by
NM, 16May2004.)



Theorem  fof 5268 
An onto mapping is a mapping. (Contributed by NM, 3Aug1994.)



Theorem  fofun 5269 
An onto mapping is a function. (Contributed by NM, 29Mar2008.)



Theorem  fofn 5270 
An onto mapping is a function on its domain. (Contributed by NM,
16Dec2008.)



Theorem  forn 5271 
The codomain of an onto function is its range. (Contributed by NM,
3Aug1994.)



Theorem  dffo2 5272 
Alternate definition of an onto function. (Contributed by NM,
22Mar2006.)



Theorem  foima 5273 
The image of the domain of an onto function. (Contributed by NM,
29Nov2002.)



Theorem  dffn4 5274 
A function maps onto its range. (Contributed by NM, 10May1998.)



Theorem  funforn 5275 
A function maps its domain onto its range. (Contributed by NM,
23Jul2004.)



Theorem  fodmrnu 5276 
An onto function has unique domain and range. (Contributed by NM,
5Nov2006.)



Theorem  fores 5277 
Restriction of a function. (Contributed by NM, 4Mar1997.)



Theorem  foco 5278 
Composition of onto functions. (Contributed by NM, 22Mar2006.)



Theorem  f1oeq1 5279 
Equality theorem for onetoone onto functions. (Contributed by NM,
10Feb1997.)



Theorem  f1oeq2 5280 
Equality theorem for onetoone onto functions. (Contributed by NM,
10Feb1997.)



Theorem  f1oeq3 5281 
Equality theorem for onetoone onto functions. (Contributed by NM,
10Feb1997.)



Theorem  f1oeq23 5282 
Equality theorem for onetoone onto functions. (Contributed by FL,
14Jul2012.)



Theorem  f1eq123d 5283 
Equality deduction for onetoone functions. (Contributed by Mario
Carneiro, 27Jan2017.)



Theorem  foeq123d 5284 
Equality deduction for onto functions. (Contributed by Mario Carneiro,
27Jan2017.)



Theorem  f1oeq123d 5285 
Equality deduction for onetoone onto functions. (Contributed by Mario
Carneiro, 27Jan2017.)



Theorem  nff1o 5286 
Boundvariable hypothesis builder for a onetoone onto function.
(Contributed by NM, 16May2004.)



Theorem  f1of1 5287 
A onetoone onto mapping is a onetoone mapping. (Contributed by NM,
12Dec2003.)



Theorem  f1of 5288 
A onetoone onto mapping is a mapping. (Contributed by NM,
12Dec2003.)



Theorem  f1ofn 5289 
A onetoone onto mapping is function on its domain. (Contributed by NM,
12Dec2003.)



Theorem  f1ofun 5290 
A onetoone onto mapping is a function. (Contributed by NM,
12Dec2003.)



Theorem  f1orel 5291 
A onetoone onto mapping is a relation. (Contributed by NM,
13Dec2003.)



Theorem  f1odm 5292 
The domain of a onetoone onto mapping. (Contributed by NM,
8Mar2014.)



Theorem  dff1o2 5293 
Alternate definition of onetoone onto function. (Contributed by NM,
10Feb1997.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  dff1o3 5294 
Alternate definition of onetoone onto function. (Contributed by NM,
25Mar1998.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  f1ofo 5295 
A onetoone onto function is an onto function. (Contributed by NM,
28Apr2004.)



Theorem  dff1o4 5296 
Alternate definition of onetoone onto function. (Contributed by NM,
25Mar1998.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  dff1o5 5297 
Alternate definition of onetoone onto function. (Contributed by NM,
10Dec2003.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  f1orn 5298 
A onetoone function maps onto its range. (Contributed by NM,
13Aug2004.)



Theorem  f1f1orn 5299 
A onetoone function maps onetoone onto its range. (Contributed by NM,
4Sep2004.)



Theorem  f1oabexg 5300* 
The class of all 11onto functions mapping one set to another is a set.
(Contributed by Paul Chapman, 25Feb2008.)

