Type  Label  Description 
Statement 

Theorem  funss 5001 
Subclass theorem for function predicate. (Contributed by NM,
16Aug1994.) (Proof shortened by Mario Carneiro, 24Jun2014.)



Theorem  funeq 5002 
Equality theorem for function predicate. (Contributed by NM,
16Aug1994.)



Theorem  funeqi 5003 
Equality inference for the function predicate. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  funeqd 5004 
Equality deduction for the function predicate. (Contributed by NM,
23Feb2013.)



Theorem  nffun 5005 
Boundvariable hypothesis builder for a function. (Contributed by NM,
30Jan2004.)



Theorem  sbcfung 5006 
Distribute proper substitution through the function predicate.
(Contributed by Alexander van der Vekens, 23Jul2017.)



Theorem  funeu 5007* 
There is exactly one value of a function. (Contributed by NM,
22Apr2004.) (Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  funeu2 5008* 
There is exactly one value of a function. (Contributed by NM,
3Aug1994.)



Theorem  dffun7 5009* 
Alternate definition of a function. One possibility for the definition
of a function in [Enderton] p. 42.
(Enderton's definition is ambiguous
because "there is only one" could mean either "there is
at most one" or
"there is exactly one." However, dffun8 5010 shows that it doesn't matter
which meaning we pick.) (Contributed by NM, 4Nov2002.)



Theorem  dffun8 5010* 
Alternate definition of a function. One possibility for the definition
of a function in [Enderton] p. 42.
Compare dffun7 5009. (Contributed by
NM, 4Nov2002.) (Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  dffun9 5011* 
Alternate definition of a function. (Contributed by NM, 28Mar2007.)
(Revised by NM, 16Jun2017.)



Theorem  funfn 5012 
An equivalence for the function predicate. (Contributed by NM,
13Aug2004.)



Theorem  funi 5013 
The identity relation is a function. Part of Theorem 10.4 of [Quine]
p. 65. (Contributed by NM, 30Apr1998.)



Theorem  nfunv 5014 
The universe is not a function. (Contributed by Raph Levien,
27Jan2004.)



Theorem  funopg 5015 
A Kuratowski ordered pair is a function only if its components are
equal. (Contributed by NM, 5Jun2008.) (Revised by Mario Carneiro,
26Apr2015.)



Theorem  funopab 5016* 
A class of ordered pairs is a function when there is at most one second
member for each pair. (Contributed by NM, 16May1995.)



Theorem  funopabeq 5017* 
A class of ordered pairs of values is a function. (Contributed by NM,
14Nov1995.)



Theorem  funopab4 5018* 
A class of ordered pairs of values in the form used by dfmpt 3878 is a
function. (Contributed by NM, 17Feb2013.)



Theorem  funmpt 5019 
A function in mapsto notation is a function. (Contributed by Mario
Carneiro, 13Jan2013.)



Theorem  funmpt2 5020 
Functionality of a class given by a mapsto notation. (Contributed by
FL, 17Feb2008.) (Revised by Mario Carneiro, 31May2014.)



Theorem  funco 5021 
The composition of two functions is a function. Exercise 29 of
[TakeutiZaring] p. 25.
(Contributed by NM, 26Jan1997.) (Proof
shortened by Andrew Salmon, 17Sep2011.)



Theorem  funres 5022 
A restriction of a function is a function. Compare Exercise 18 of
[TakeutiZaring] p. 25. (Contributed
by NM, 16Aug1994.)



Theorem  funssres 5023 
The restriction of a function to the domain of a subclass equals the
subclass. (Contributed by NM, 15Aug1994.)



Theorem  fun2ssres 5024 
Equality of restrictions of a function and a subclass. (Contributed by
NM, 16Aug1994.)



Theorem  funun 5025 
The union of functions with disjoint domains is a function. Theorem 4.6
of [Monk1] p. 43. (Contributed by NM,
12Aug1994.)



Theorem  funcnvsn 5026 
The converse singleton of an ordered pair is a function. This is
equivalent to funsn 5029 via cnvsn 4881, but stating it this way allows us to
skip the sethood assumptions on and . (Contributed by NM,
30Apr2015.)



Theorem  funsng 5027 
A singleton of an ordered pair is a function. Theorem 10.5 of [Quine]
p. 65. (Contributed by NM, 28Jun2011.)



Theorem  fnsng 5028 
Functionality and domain of the singleton of an ordered pair.
(Contributed by Mario Carneiro, 30Apr2015.)



Theorem  funsn 5029 
A singleton of an ordered pair is a function. Theorem 10.5 of [Quine]
p. 65. (Contributed by NM, 12Aug1994.)



Theorem  funinsn 5030 
A function based on the singleton of an ordered pair. Unlike funsng 5027,
this holds even if or is a
proper class. (Contributed by
Jim Kingdon, 17Apr2022.)



Theorem  funprg 5031 
A set of two pairs is a function if their first members are different.
(Contributed by FL, 26Jun2011.)



Theorem  funtpg 5032 
A set of three pairs is a function if their first members are different.
(Contributed by Alexander van der Vekens, 5Dec2017.)



Theorem  funpr 5033 
A function with a domain of two elements. (Contributed by Jeff Madsen,
20Jun2010.)



Theorem  funtp 5034 
A function with a domain of three elements. (Contributed by NM,
14Sep2011.)



Theorem  fnsn 5035 
Functionality and domain of the singleton of an ordered pair.
(Contributed by Jonathan BenNaim, 3Jun2011.)



Theorem  fnprg 5036 
Function with a domain of two different values. (Contributed by FL,
26Jun2011.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  fntpg 5037 
Function with a domain of three different values. (Contributed by
Alexander van der Vekens, 5Dec2017.)



Theorem  fntp 5038 
A function with a domain of three elements. (Contributed by NM,
14Sep2011.) (Revised by Mario Carneiro, 26Apr2015.)



Theorem  fun0 5039 
The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed
by NM, 7Apr1998.)



Theorem  funcnvcnv 5040 
The double converse of a function is a function. (Contributed by NM,
21Sep2004.)



Theorem  funcnv2 5041* 
A simpler equivalence for singlerooted (see funcnv 5042). (Contributed
by NM, 9Aug2004.)



Theorem  funcnv 5042* 
The converse of a class is a function iff the class is singlerooted,
which means that for any in the range of there is at most
one such that
. Definition of singlerooted in
[Enderton] p. 43. See funcnv2 5041 for a simpler version. (Contributed by
NM, 13Aug2004.)



Theorem  funcnv3 5043* 
A condition showing a class is singlerooted. (See funcnv 5042).
(Contributed by NM, 26May2006.)



Theorem  funcnveq 5044* 
Another way of expressing that a class is singlerooted. Counterpart to
dffun2 4993. (Contributed by Jim Kingdon, 24Dec2018.)



Theorem  fun2cnv 5045* 
The double converse of a class is a function iff the class is
singlevalued. Each side is equivalent to Definition 6.4(2) of
[TakeutiZaring] p. 23, who use the
notation "Un(A)" for singlevalued.
Note that is
not necessarily a function. (Contributed by NM,
13Aug2004.)



Theorem  svrelfun 5046 
A singlevalued relation is a function. (See fun2cnv 5045 for
"singlevalued.") Definition 6.4(4) of [TakeutiZaring] p. 24.
(Contributed by NM, 17Jan2006.)



Theorem  fncnv 5047* 
Singlerootedness (see funcnv 5042) of a class cut down by a cross
product. (Contributed by NM, 5Mar2007.)



Theorem  fun11 5048* 
Two ways of stating that is onetoone (but not necessarily a
function). Each side is equivalent to Definition 6.4(3) of
[TakeutiZaring] p. 24, who use the
notation "Un_{2} (A)" for onetoone
(but not necessarily a function). (Contributed by NM, 17Jan2006.)



Theorem  fununi 5049* 
The union of a chain (with respect to inclusion) of functions is a
function. (Contributed by NM, 10Aug2004.)



Theorem  funcnvuni 5050* 
The union of a chain (with respect to inclusion) of singlerooted sets
is singlerooted. (See funcnv 5042 for "singlerooted"
definition.)
(Contributed by NM, 11Aug2004.)



Theorem  fun11uni 5051* 
The union of a chain (with respect to inclusion) of onetoone functions
is a onetoone function. (Contributed by NM, 11Aug2004.)



Theorem  funin 5052 
The intersection with a function is a function. Exercise 14(a) of
[Enderton] p. 53. (Contributed by NM,
19Mar2004.) (Proof shortened by
Andrew Salmon, 17Sep2011.)



Theorem  funres11 5053 
The restriction of a onetoone function is onetoone. (Contributed by
NM, 25Mar1998.)



Theorem  funcnvres 5054 
The converse of a restricted function. (Contributed by NM,
27Mar1998.)



Theorem  cnvresid 5055 
Converse of a restricted identity function. (Contributed by FL,
4Mar2007.)



Theorem  funcnvres2 5056 
The converse of a restriction of the converse of a function equals the
function restricted to the image of its converse. (Contributed by NM,
4May2005.)



Theorem  funimacnv 5057 
The image of the preimage of a function. (Contributed by NM,
25May2004.)



Theorem  funimass1 5058 
A kind of contraposition law that infers a subclass of an image from a
preimage subclass. (Contributed by NM, 25May2004.)



Theorem  funimass2 5059 
A kind of contraposition law that infers an image subclass from a subclass
of a preimage. (Contributed by NM, 25May2004.)



Theorem  imadiflem 5060 
One direction of imadif 5061. This direction does not require
. (Contributed by Jim Kingdon,
25Dec2018.)



Theorem  imadif 5061 
The image of a difference is the difference of images. (Contributed by
NM, 24May1998.)



Theorem  imainlem 5062 
One direction of imain 5063. This direction does not require
. (Contributed by Jim Kingdon,
25Dec2018.)



Theorem  imain 5063 
The image of an intersection is the intersection of images.
(Contributed by Paul Chapman, 11Apr2009.)



Theorem  funimaexglem 5064 
Lemma for funimaexg 5065. It constitutes the interesting part of
funimaexg 5065, in which
. (Contributed by Jim
Kingdon,
27Dec2018.)



Theorem  funimaexg 5065 
Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284.
Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM,
10Sep2006.)



Theorem  funimaex 5066 
The image of a set under any function is also a set. Equivalent of
Axiom of Replacement. Axiom 39(vi) of [Quine] p. 284. Compare Exercise
9 of [TakeutiZaring] p. 29.
(Contributed by NM, 17Nov2002.)



Theorem  isarep1 5067* 
Part of a study of the Axiom of Replacement used by the Isabelle prover.
The object PrimReplace is apparently the image of the function encoded
by i.e. the class .
If so, we can prove Isabelle's "Axiom of Replacement"
conclusion without
using the Axiom of Replacement, for which I (N. Megill) currently have
no explanation. (Contributed by NM, 26Oct2006.) (Proof shortened by
Mario Carneiro, 4Dec2016.)



Theorem  isarep2 5068* 
Part of a study of the Axiom of Replacement used by the Isabelle prover.
In Isabelle, the sethood of PrimReplace is apparently postulated
implicitly by its type signature " i, i, i
=> o
=> i", which automatically asserts that it is a set without
using any
axioms. To prove that it is a set in Metamath, we need the hypotheses
of Isabelle's "Axiom of Replacement" as well as the Axiom of
Replacement
in the form funimaex 5066. (Contributed by NM, 26Oct2006.)



Theorem  fneq1 5069 
Equality theorem for function predicate with domain. (Contributed by NM,
1Aug1994.)



Theorem  fneq2 5070 
Equality theorem for function predicate with domain. (Contributed by NM,
1Aug1994.)



Theorem  fneq1d 5071 
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22Jun2011.)



Theorem  fneq2d 5072 
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22Jun2011.)



Theorem  fneq12d 5073 
Equality deduction for function predicate with domain. (Contributed by
NM, 26Jun2011.)



Theorem  fneq12 5074 
Equality theorem for function predicate with domain. (Contributed by
Thierry Arnoux, 31Jan2017.)



Theorem  fneq1i 5075 
Equality inference for function predicate with domain. (Contributed by
Paul Chapman, 22Jun2011.)



Theorem  fneq2i 5076 
Equality inference for function predicate with domain. (Contributed by
NM, 4Sep2011.)



Theorem  nffn 5077 
Boundvariable hypothesis builder for a function with domain.
(Contributed by NM, 30Jan2004.)



Theorem  fnfun 5078 
A function with domain is a function. (Contributed by NM, 1Aug1994.)



Theorem  fnrel 5079 
A function with domain is a relation. (Contributed by NM, 1Aug1994.)



Theorem  fndm 5080 
The domain of a function. (Contributed by NM, 2Aug1994.)



Theorem  funfni 5081 
Inference to convert a function and domain antecedent. (Contributed by
NM, 22Apr2004.)



Theorem  fndmu 5082 
A function has a unique domain. (Contributed by NM, 11Aug1994.)



Theorem  fnbr 5083 
The first argument of binary relation on a function belongs to the
function's domain. (Contributed by NM, 7May2004.)



Theorem  fnop 5084 
The first argument of an ordered pair in a function belongs to the
function's domain. (Contributed by NM, 8Aug1994.)



Theorem  fneu 5085* 
There is exactly one value of a function. (Contributed by NM,
22Apr2004.) (Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fneu2 5086* 
There is exactly one value of a function. (Contributed by NM,
7Nov1995.)



Theorem  fnun 5087 
The union of two functions with disjoint domains. (Contributed by NM,
22Sep2004.)



Theorem  fnunsn 5088 
Extension of a function with a new ordered pair. (Contributed by NM,
28Sep2013.) (Revised by Mario Carneiro, 30Apr2015.)



Theorem  fnco 5089 
Composition of two functions. (Contributed by NM, 22May2006.)



Theorem  fnresdm 5090 
A function does not change when restricted to its domain. (Contributed by
NM, 5Sep2004.)



Theorem  fnresdisj 5091 
A function restricted to a class disjoint with its domain is empty.
(Contributed by NM, 23Sep2004.)



Theorem  2elresin 5092 
Membership in two functions restricted by each other's domain.
(Contributed by NM, 8Aug1994.)



Theorem  fnssresb 5093 
Restriction of a function with a subclass of its domain. (Contributed by
NM, 10Oct2007.)



Theorem  fnssres 5094 
Restriction of a function with a subclass of its domain. (Contributed by
NM, 2Aug1994.)



Theorem  fnresin1 5095 
Restriction of a function's domain with an intersection. (Contributed by
NM, 9Aug1994.)



Theorem  fnresin2 5096 
Restriction of a function's domain with an intersection. (Contributed by
NM, 9Aug1994.)



Theorem  fnres 5097* 
An equivalence for functionality of a restriction. Compare dffun8 5010.
(Contributed by Mario Carneiro, 20May2015.)



Theorem  fnresi 5098 
Functionality and domain of restricted identity. (Contributed by NM,
27Aug2004.)



Theorem  fnima 5099 
The image of a function's domain is its range. (Contributed by NM,
4Nov2004.) (Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fn0 5100 
A function with empty domain is empty. (Contributed by NM, 15Apr1998.)
(Proof shortened by Andrew Salmon, 17Sep2011.)

