Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  f1ff1 5336 
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 5337 
A function that is onetoone is also onetoone on any subclass of its
domain. (Contributed by Mario Carneiro, 17Jan2015.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  f1oeq2d 5363 
Equality deduction for onetoone onto functions. (Contributed by
Glauco Siliprandi, 17Aug2020.)



Theorem  f1oeq3d 5364 
Equality deduction for onetoone onto functions. (Contributed by
Glauco Siliprandi, 17Aug2020.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

