Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  f1cnvcnv 5043 
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 5044 
Composition of onetoone functions. Exercise 30 of [TakeutiZaring]
p. 25. (Contributed by NM, 28May1998.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  f1ocnv 5082 
The converse of a onetoone onto function is also onetoone onto.
(Contributed by NM, 11Feb1997.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  f1ocnvb 5083 
A relation is a onetoone onto function iff its converse is a onetoone
onto function with domain and range interchanged. (Contributed by NM,
8Dec2003.)



Theorem  f1ores 5084 
The restriction of a onetoone function maps onetoone onto the image.
(Contributed by NM, 25Mar1998.)



Theorem  f1orescnv 5085 
The converse of a onetooneonto restricted function. (Contributed by
Paul Chapman, 21Apr2008.)



Theorem  f1imacnv 5086 
Preimage of an image. (Contributed by NM, 30Sep2004.)



Theorem  foimacnv 5087 
A reverse version of f1imacnv 5086. (Contributed by Jeff Hankins,
16Jul2009.)



Theorem  foun 5088 
The union of two onto functions with disjoint domains is an onto
function. (Contributed by Mario Carneiro, 22Jun2016.)



Theorem  f1oun 5089 
The union of two onetoone onto functions with disjoint domains and
ranges. (Contributed by NM, 26Mar1998.)



Theorem  fun11iun 5090* 
The union of a chain (with respect to inclusion) of onetoone functions
is a onetoone function. (Contributed by Mario Carneiro,
20May2013.) (Revised by Mario Carneiro, 24Jun2015.)



Theorem  resdif 5091 
The restriction of a onetoone onto function to a difference maps onto
the difference of the images. (Contributed by Paul Chapman,
11Apr2009.)



Theorem  f1oco 5092 
Composition of onetoone onto functions. (Contributed by NM,
19Mar1998.)



Theorem  f1cnv 5093 
The converse of an injective function is bijective. (Contributed by FL,
11Nov2011.)



Theorem  funcocnv2 5094 
Composition with the converse. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  fococnv2 5095 
The composition of an onto function and its converse. (Contributed by
Stefan O'Rear, 12Feb2015.)



Theorem  f1ococnv2 5096 
The composition of a onetoone onto function and its converse equals the
identity relation restricted to the function's range. (Contributed by NM,
13Dec2003.) (Proof shortened by Stefan O'Rear, 12Feb2015.)



Theorem  f1cocnv2 5097 
Composition of an injective function with its converse. (Contributed by
FL, 11Nov2011.)



Theorem  f1ococnv1 5098 
The composition of a onetoone onto function's converse and itself equals
the identity relation restricted to the function's domain. (Contributed
by NM, 13Dec2003.)



Theorem  f1cocnv1 5099 
Composition of an injective function with its converse. (Contributed by
FL, 11Nov2011.)



Theorem  funcoeqres 5100 
Reexpress a constraint on a composition as a constraint on the
composand. (Contributed by Stefan O'Rear, 7Mar2015.)

