Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  funcnv 5120* 
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 5119 for a simpler version. (Contributed by
NM, 13Aug2004.)



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



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



Theorem  fun2cnv 5123* 
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 5124 
A singlevalued relation is a function. (See fun2cnv 5123 for
"singlevalued.") Definition 6.4(4) of [TakeutiZaring] p. 24.
(Contributed by NM, 17Jan2006.)



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



Theorem  fun11 5126* 
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 5127* 
The union of a chain (with respect to inclusion) of functions is a
function. (Contributed by NM, 10Aug2004.)



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



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



Theorem  funin 5130 
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 5131 
The restriction of a onetoone function is onetoone. (Contributed by
NM, 25Mar1998.)



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



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



Theorem  funcnvres2 5134 
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 5135 
The image of the preimage of a function. (Contributed by NM,
25May2004.)



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



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



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



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



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



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



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



Theorem  funimaexg 5143 
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 5144 
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 5145* 
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 5146* 
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 5144. (Contributed by NM, 26Oct2006.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  fnimadisj 5179 
A class that is disjoint with the domain of a function has an empty image
under the function. (Contributed by FL, 24Jan2007.)



Theorem  fnimaeq0 5180 
Images under a function never map nonempty sets to empty sets.
(Contributed by Stefan O'Rear, 21Jan2015.)



Theorem  dfmpt3 5181 
Alternate definition for the mapsto notation dfmpt 3931. (Contributed
by Mario Carneiro, 30Dec2016.)



Theorem  fnopabg 5182* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by NM, 30Jan2004.) (Proof shortened by Mario Carneiro,
4Dec2016.)



Theorem  fnopab 5183* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by NM, 5Mar1996.)



Theorem  mptfng 5184* 
The mapsto notation defines a function with domain. (Contributed by
Scott Fenton, 21Mar2011.)



Theorem  fnmpt 5185* 
The mapsto notation defines a function with domain. (Contributed by
NM, 9Apr2013.)



Theorem  mpt0 5186 
A mapping operation with empty domain. (Contributed by Mario Carneiro,
28Dec2014.)



Theorem  fnmpti 5187* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by NM, 29Jan2004.) (Revised by Mario Carneiro,
31Aug2015.)



Theorem  dmmpti 5188* 
Domain of an orderedpair class abstraction that specifies a function.
(Contributed by NM, 6Sep2005.) (Revised by Mario Carneiro,
31Aug2015.)



Theorem  dmmptd 5189* 
The domain of the mapping operation, deduction form. (Contributed by
Glauco Siliprandi, 11Dec2019.)



Theorem  mptun 5190 
Union of mappings which are mutually compatible. (Contributed by Mario
Carneiro, 31Aug2015.)



Theorem  feq1 5191 
Equality theorem for functions. (Contributed by NM, 1Aug1994.)



Theorem  feq2 5192 
Equality theorem for functions. (Contributed by NM, 1Aug1994.)



Theorem  feq3 5193 
Equality theorem for functions. (Contributed by NM, 1Aug1994.)



Theorem  feq23 5194 
Equality theorem for functions. (Contributed by FL, 14Jul2007.) (Proof
shortened by Andrew Salmon, 17Sep2011.)



Theorem  feq1d 5195 
Equality deduction for functions. (Contributed by NM, 19Feb2008.)



Theorem  feq2d 5196 
Equality deduction for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq3d 5197 
Equality deduction for functions. (Contributed by AV, 1Jan2020.)



Theorem  feq12d 5198 
Equality deduction for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq123d 5199 
Equality deduction for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq123 5200 
Equality theorem for functions. (Contributed by FL, 16Nov2008.)

