Type  Label  Description 
Statement 

Theorem  fnima 5201 
The image of a function's domain is its range. (The proof was shortened
by Andrew Salmon, 17Sep2011.) (Contributed by set.mm contributors,
4Nov2004.) (Revised by set.mm contributors, 18Sep2011.)



Theorem  fn0 5202 
A function with empty domain is empty. (The proof was shortened by Andrew
Salmon, 17Sep2011.) (Contributed by set.mm contributors, 15Apr1998.)
(Revised by set.mm contributors, 18Sep2011.)



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



Theorem  iunfopab 5204* 
Two ways to express a function as a class of ordered pairs. (The proof
was shortened by Andrew Salmon, 17Sep2011.) (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19Sep2011.)
(Contributed by set.mm contributors, 19Dec2008.)



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



Theorem  fnopab2g 5206* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by set.mm contributors, 23Mar2006.)



Theorem  fnopab 5207* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by set.mm contributors, 5Mar1996.)



Theorem  fnopab2 5208* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by set.mm contributors, 29Jan2004.)



Theorem  dmopab2 5209* 
Domain of an orderedpair class abstraction that specifies a function.
(Contributed by set.mm contributors, 6Sep2005.)



Theorem  feq1 5210 
Equality theorem for functions. (Contributed by set.mm contributors,
1Aug1994.)



Theorem  feq2 5211 
Equality theorem for functions. (Contributed by set.mm contributors,
1Aug1994.)



Theorem  feq3 5212 
Equality theorem for functions. (Contributed by set.mm contributors,
1Aug1994.)



Theorem  feq23 5213 
Equality theorem for functions. (Contributed by FL, 14Jul2007.) (The
proof was shortened by Andrew Salmon, 17Sep2011.)



Theorem  feq1d 5214 
Equality deduction for functions. (Contributed by set.mm contributors,
19Feb2008.)



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



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



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



Theorem  feq2i 5218 
Equality inference for functions. (Contributed by set.mm contributors,
5Sep2011.)



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



Theorem  feq23d 5220 
Equality deduction for functions. (Contributed by set.mm contributors,
8Jun2013.)



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



Theorem  elimf 5222 
Eliminate a mapping hypothesis for the weak deduction theorem dedth 3703,
when a special case is provable, in order to
convert
from a hypothesis to an antecedent. (Contributed by
set.mm contributors, 24Aug2006.)



Theorem  ffn 5223 
A mapping is a function. (Contributed by set.mm contributors,
2Aug1994.)



Theorem  dffn2 5224 
Any function is a mapping into . (The proof was shortened by
Andrew Salmon, 17Sep2011.) (Contributed by set.mm contributors,
31Oct1995.) (Revised by set.mm contributors, 18Sep2011.)



Theorem  ffun 5225 
A mapping is a function. (Contributed by set.mm contributors,
3Aug1994.)



Theorem  fdm 5226 
The domain of a mapping. (Contributed by set.mm contributors,
2Aug1994.)



Theorem  fdmi 5227 
The domain of a mapping. (Contributed by set.mm contributors,
28Jul2008.)



Theorem  frn 5228 
The range of a mapping. (Contributed by set.mm contributors,
3Aug1994.)



Theorem  dffn3 5229 
A function maps to its range. (Contributed by set.mm contributors,
1Sep1999.)



Theorem  fss 5230 
Expanding the codomain of a mapping. (The proof was shortened by Andrew
Salmon, 17Sep2011.) (Contributed by set.mm contributors, 10May1998.)
(Revised by set.mm contributors, 18Sep2011.)



Theorem  fco 5231 
Composition of two mappings. (The proof was shortened by Andrew Salmon,
17Sep2011.) (Contributed by set.mm contributors, 29Aug1999.)
(Revised by set.mm contributors, 18Sep2011.)



Theorem  fssxp 5232 
A mapping is a class of ordered pairs. (The proof was shortened by Andrew
Salmon, 17Sep2011.) (Contributed by set.mm contributors, 3Aug1994.)
(Revised by set.mm contributors, 18Sep2011.)



Theorem  funssxp 5233 
Two ways of specifying a partial function from to .
(Contributed by set.mm contributors, 13Nov2007.)



Theorem  ffdm 5234 
A mapping is a partial function. (Contributed by set.mm contributors,
25Nov2007.)



Theorem  opelf 5235 
The members of an ordered pair element of a mapping belong to the
mapping's domain and codomain. (Contributed by set.mm contributors,
9Jan2015.)



Theorem  fun 5236 
The union of two functions with disjoint domains. (Contributed by set.mm
contributors, 22Sep2004.)



Theorem  fnfco 5237 
Composition of two functions. (Contributed by set.mm contributors,
22May2006.)



Theorem  fssres 5238 
Restriction of a function with a subclass of its domain. (Contributed by
set.mm contributors, 23Sep2004.)



Theorem  fssres2 5239 
Restriction of a restricted function with a subclass of its domain.
(Contributed by set.mm contributors, 21Jul2005.)



Theorem  fcoi1 5240 
Composition of a mapping and restricted identity. (The proof was
shortened by Andrew Salmon, 17Sep2011.) (Contributed by set.mm
contributors, 13Dec2003.) (Revised by set.mm contributors,
18Sep2011.)



Theorem  fcoi2 5241 
Composition of restricted identity and a mapping. (The proof was
shortened by Andrew Salmon, 17Sep2011.) (Contributed by set.mm
contributors, 13Dec2003.) (Revised by set.mm contributors,
18Sep2011.)



Theorem  feu 5242* 
There is exactly one value of a function in its codomain. (Contributed
by set.mm contributors, 10Dec2003.)



Theorem  fcnvres 5243 
The converse of a restriction of a function. (Contributed by set.mm
contributors, 26Mar1998.)



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



Theorem  fint 5245* 
Function into an intersection. (The proof was shortened by Andrew
Salmon, 17Sep2011.) (Contributed by set.mm contributors,
14Oct1999.) (Revised by set.mm contributors, 18Sep2011.)



Theorem  fin 5246 
Mapping into an intersection. (The proof was shortened by Andrew Salmon,
17Sep2011.) (Contributed by set.mm contributors, 14Sep1999.)
(Revised by set.mm contributors, 18Sep2011.)



Theorem  dmfex 5247 
If a mapping is a set, its domain is a set. (The proof was shortened by
Andrew Salmon, 17Sep2011.) (Contributed by set.mm contributors,
27Aug2006.) (Revised by set.mm contributors, 18Sep2011.)



Theorem  f0 5248 
The empty function. (Contributed by set.mm contributors, 14Aug1999.)



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



Theorem  fconst 5250 
A cross product with a singleton is a constant function. (The proof was
shortened by Andrew Salmon, 17Sep2011.) (Contributed by set.mm
contributors, 14Aug1999.) (Revised by set.mm contributors,
18Sep2011.)



Theorem  fconstg 5251 
A cross product with a singleton is a constant function. (Contributed
by set.mm contributors, 19Oct2004.)



Theorem  fnconstg 5252 
A cross product with a singleton is a constant function. (Contributed
by set.mm contributors, 24Jul2014.)



Theorem  f1eq1 5253 
Equality theorem for onetoone functions. (Contributed by set.mm
contributors, 10Feb1997.)



Theorem  f1eq2 5254 
Equality theorem for onetoone functions. (Contributed by set.mm
contributors, 10Feb1997.)



Theorem  f1eq3 5255 
Equality theorem for onetoone functions. (Contributed by set.mm
contributors, 10Feb1997.)



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



Theorem  dff12 5257* 
Alternate definition of a onetoone function. (Contributed by set.mm
contributors, 31Dec1996.) (Revised by set.mm contributors,
22Sep2004.)



Theorem  f1f 5258 
A onetoone mapping is a mapping. (Contributed by set.mm contributors,
31Dec1996.)



Theorem  f1fn 5259 
A onetoone mapping is a function on its domain. (Contributed by set.mm
contributors, 8Mar2014.)



Theorem  f1fun 5260 
A onetoone mapping is a function. (Contributed by set.mm contributors,
8Mar2014.)



Theorem  f1dm 5261 
The domain of a onetoone mapping. (Contributed by set.mm contributors,
8Mar2014.)



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



Theorem  f1funfun 5263 
Two ways to express that a set 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 set.mm contributors, 13Aug2004.)
(Revised
by Scott Fenton, 18Apr2021.)



Theorem  f1co 5264 
Composition of onetoone functions. Exercise 30 of [TakeutiZaring]
p. 25. (Contributed by set.mm contributors, 28May1998.)



Theorem  foeq1 5265 
Equality theorem for onto functions. (Contributed by set.mm contributors,
1Aug1994.)



Theorem  foeq2 5266 
Equality theorem for onto functions. (Contributed by set.mm contributors,
1Aug1994.)



Theorem  foeq3 5267 
Equality theorem for onto functions. (Contributed by set.mm contributors,
1Aug1994.)



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



Theorem  fof 5269 
An onto mapping is a mapping. (Contributed by set.mm contributors,
3Aug1994.)



Theorem  fofun 5270 
An onto mapping is a function. (Contributed by set.mm contributors,
29Mar2008.)



Theorem  fofn 5271 
An onto mapping is a function on its domain. (Contributed by set.mm
contributors, 16Dec2008.)



Theorem  forn 5272 
The codomain of an onto function is its range. (Contributed by set.mm
contributors, 3Aug1994.)



Theorem  dffo2 5273 
Alternate definition of an onto function. (Contributed by set.mm
contributors, 22Mar2006.)



Theorem  foima 5274 
The image of the domain of an onto function. (Contributed by set.mm
contributors, 29Nov2002.)



Theorem  dffn4 5275 
A function maps onto its range. (Contributed by set.mm contributors,
10May1998.)



Theorem  funforn 5276 
A function maps its domain onto its range. (Contributed by set.mm
contributors, 23Jul2004.)



Theorem  fodmrnu 5277 
An onto function has unique domain and range. (Contributed by set.mm
contributors, 5Nov2006.)



Theorem  fores 5278 
Restriction of a function. (Contributed by set.mm contributors,
4Mar1997.)



Theorem  foco 5279 
Composition of onto functions. (Contributed by set.mm contributors,
22Mar2006.)



Theorem  foconst 5280 
A nonzero constant function is onto. (Contributed by set.mm contributors,
12Jan2007.)



Theorem  f1oeq1 5281 
Equality theorem for onetoone onto functions. (Contributed by set.mm
contributors, 10Feb1997.)



Theorem  f1oeq2 5282 
Equality theorem for onetoone onto functions. (Contributed by set.mm
contributors, 10Feb1997.)



Theorem  f1oeq3 5283 
Equality theorem for onetoone onto functions. (Contributed by set.mm
contributors, 10Feb1997.)



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



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



Theorem  f1of1 5286 
A onetoone onto mapping is a onetoone mapping. (Contributed by set.mm
contributors, 12Dec2003.)



Theorem  f1of 5287 
A onetoone onto mapping is a mapping. (Contributed by set.mm
contributors, 12Dec2003.)



Theorem  f1ofn 5288 
A onetoone onto mapping is function on its domain. (Contributed by
set.mm contributors, 12Dec2003.)



Theorem  f1ofun 5289 
A onetoone onto mapping is a function. (Contributed by set.mm
contributors, 12Dec2003.)



Theorem  f1odm 5290 
The domain of a onetoone onto mapping. (Contributed by set.mm
contributors, 8Mar2014.)



Theorem  dff1o2 5291 
Alternate definition of onetoone onto function. (The proof was
shortened by Andrew Salmon, 22Oct2011.) (Contributed by set.mm
contributors, 10Feb1997.) (Revised by set.mm contributors,
22Oct2011.)



Theorem  dff1o3 5292 
Alternate definition of onetoone onto function. (The proof was
shortened by Andrew Salmon, 22Oct2011.) (Contributed by set.mm
contributors, 25Mar1998.) (Revised by set.mm contributors,
22Oct2011.)



Theorem  f1ofo 5293 
A onetoone onto function is an onto function. (Contributed by set.mm
contributors, 28Apr2004.)



Theorem  dff1o4 5294 
Alternate definition of onetoone onto function. (The proof was
shortened by Andrew Salmon, 22Oct2011.) (Contributed by set.mm
contributors, 25Mar1998.) (Revised by set.mm contributors,
22Oct2011.)



Theorem  dff1o5 5295 
Alternate definition of onetoone onto function. (The proof was
shortened by Andrew Salmon, 22Oct2011.) (Contributed by set.mm
contributors, 10Dec2003.) (Revised by set.mm contributors,
22Oct2011.)



Theorem  f1orn 5296 
A onetoone function maps onto its range. (Contributed by set.mm
contributors, 13Aug2004.)



Theorem  f1f1orn 5297 
A onetoone function maps onetoone onto its range. (Contributed by
set.mm contributors, 4Sep2004.)



Theorem  f1ocnvb 5298 
A class is a onetoone onto function iff its converse is a onetoone
onto function with domain and range interchanged. (Contributed by set.mm
contributors, 8Dec2003.) (Modified by Scott Fenton, 17Apr2021.)



Theorem  f1ocnv 5299 
The converse of a onetoone onto function is also onetoone onto. (The
proof was shortened by Andrew Salmon, 22Oct2011.) (Contributed by
set.mm contributors, 11Feb1997.) (Revised by set.mm contributors,
22Oct2011.)



Theorem  f1ores 5300 
The restriction of a onetoone function maps onetoone onto the image.
(Contributed by set.mm contributors, 25Mar1998.)

