Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  f1ocnvb 5168 
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 5169 
The restriction of a onetoone function maps onetoone onto the image.
(Contributed by NM, 25Mar1998.)



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



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



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



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



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



Theorem  fun11iun 5175* 
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 5176 
The restriction of a onetoone onto function to a difference maps onto
the difference of the images. (Contributed by Paul Chapman,
11Apr2009.)



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



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



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



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



Theorem  f1ococnv2 5181 
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 5182 
Composition of an injective function with its converse. (Contributed by
FL, 11Nov2011.)



Theorem  f1ococnv1 5183 
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 5184 
Composition of an injective function with its converse. (Contributed by
FL, 11Nov2011.)



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



Theorem  ffoss 5186* 
Relationship between a mapping and an onto mapping. Figure 38 of
[Enderton] p. 145. (Contributed by NM,
10May1998.)



Theorem  f11o 5187* 
Relationship between onetoone and onetoone onto function.
(Contributed by NM, 4Apr1998.)



Theorem  f10 5188 
The empty set maps onetoone into any class. (Contributed by NM,
7Apr1998.)



Theorem  f1o00 5189 
Onetoone onto mapping of the empty set. (Contributed by NM,
15Apr1998.)



Theorem  fo00 5190 
Onto mapping of the empty set. (Contributed by NM, 22Mar2006.)



Theorem  f1o0 5191 
Onetoone onto mapping of the empty set. (Contributed by NM,
10Sep2004.)



Theorem  f1oi 5192 
A restriction of the identity relation is a onetoone onto function.
(Contributed by NM, 30Apr1998.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  f1ovi 5193 
The identity relation is a onetoone onto function on the universe.
(Contributed by NM, 16May2004.)



Theorem  f1osn 5194 
A singleton of an ordered pair is onetoone onto function.
(Contributed by NM, 18May1998.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  f1osng 5195 
A singleton of an ordered pair is onetoone onto function.
(Contributed by Mario Carneiro, 12Jan2013.)



Theorem  f1oprg 5196 
An unordered pair of ordered pairs with different elements is a onetoone
onto function. (Contributed by Alexander van der Vekens, 14Aug2017.)



Theorem  tz6.122 5197* 
Function value when
is not a function. Theorem 6.12(2) of
[TakeutiZaring] p. 27.
(Contributed by NM, 30Apr2004.) (Proof
shortened by Mario Carneiro, 31Aug2015.)



Theorem  fveu 5198* 
The value of a function at a unique point. (Contributed by Scott
Fenton, 6Oct2017.)



Theorem  brprcneu 5199* 
If is a proper class,
then there is no unique binary relationship
with as the
first element. (Contributed by Scott Fenton,
7Oct2017.)



Theorem  fvprc 5200 
A function's value at a proper class is the empty set. (Contributed by
NM, 20May1998.)

