Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  f1sng 5471 
A singleton of an ordered pair is a onetoone function. (Contributed
by AV, 17Apr2021.)



Theorem  fsnd 5472 
A singleton of an ordered pair is a function. (Contributed by AV,
17Apr2021.)



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



Theorem  tz6.122 5474* 
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 5475* 
The value of a function at a unique point. (Contributed by Scott
Fenton, 6Oct2017.)



Theorem  brprcneu 5476* 
If is a proper class
and is any class,
then there is no
unique set which is related to through the binary relation .
(Contributed by Scott Fenton, 7Oct2017.)



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



Theorem  fv2 5478* 
Alternate definition of function value. Definition 10.11 of [Quine]
p. 68. (Contributed by NM, 30Apr2004.) (Proof shortened by Andrew
Salmon, 17Sep2011.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  dffv3g 5479* 
A definition of function value in terms of iota. (Contributed by Jim
Kingdon, 29Dec2018.)



Theorem  dffv4g 5480* 
The previous definition of function value, from before the
operator was introduced. Although based on the idea embodied by
Definition 10.2 of [Quine] p. 65 (see args 4970), this definition
apparently does not appear in the literature. (Contributed by NM,
1Aug1994.)



Theorem  elfv 5481* 
Membership in a function value. (Contributed by NM, 30Apr2004.)



Theorem  fveq1 5482 
Equality theorem for function value. (Contributed by NM,
29Dec1996.)



Theorem  fveq2 5483 
Equality theorem for function value. (Contributed by NM,
29Dec1996.)



Theorem  fveq1i 5484 
Equality inference for function value. (Contributed by NM,
2Sep2003.)



Theorem  fveq1d 5485 
Equality deduction for function value. (Contributed by NM,
2Sep2003.)



Theorem  fveq2i 5486 
Equality inference for function value. (Contributed by NM,
28Jul1999.)



Theorem  fveq2d 5487 
Equality deduction for function value. (Contributed by NM,
29May1999.)



Theorem  2fveq3 5488 
Equality theorem for nested function values. (Contributed by AV,
14Aug2022.)



Theorem  fveq12i 5489 
Equality deduction for function value. (Contributed by FL,
27Jun2014.)



Theorem  fveq12d 5490 
Equality deduction for function value. (Contributed by FL,
22Dec2008.)



Theorem  fveqeq2d 5491 
Equality deduction for function value. (Contributed by BJ,
30Aug2022.)



Theorem  fveqeq2 5492 
Equality deduction for function value. (Contributed by BJ,
31Aug2022.)



Theorem  nffv 5493 
Boundvariable hypothesis builder for function value. (Contributed by
NM, 14Nov1995.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  nffvmpt1 5494* 
Boundvariable hypothesis builder for mapping, special case.
(Contributed by Mario Carneiro, 25Dec2016.)



Theorem  nffvd 5495 
Deduction version of boundvariable hypothesis builder nffv 5493.
(Contributed by NM, 10Nov2005.) (Revised by Mario Carneiro,
15Oct2016.)



Theorem  funfveu 5496* 
A function has one value given an argument in its domain. (Contributed
by Jim Kingdon, 29Dec2018.)



Theorem  fvss 5497* 
The value of a function is a subset of if every element that could
be a candidate for the value is a subset of . (Contributed by
Mario Carneiro, 24May2019.)



Theorem  fvssunirng 5498 
The result of a function value is always a subset of the union of the
range, if the input is a set. (Contributed by Stefan O'Rear,
2Nov2014.) (Revised by Mario Carneiro, 24May2019.)



Theorem  relfvssunirn 5499 
The result of a function value is always a subset of the union of the
range, even if it is invalid and thus empty. (Contributed by Stefan
O'Rear, 2Nov2014.) (Revised by Mario Carneiro, 24May2019.)



Theorem  funfvex 5500 
The value of a function exists. A special case of Corollary 6.13 of
[TakeutiZaring] p. 27.
(Contributed by Jim Kingdon, 29Dec2018.)

