Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



Theorem  funimaexg 5011 
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 5012 
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 5013* 
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 5014* 
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 5012. (Contributed by NM, 26Oct2006.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  dfmpt3 5049 
Alternate definition for the "maps to" notation dfmpt 3848. (Contributed
by Mario Carneiro, 30Dec2016.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  feq1i 5067 
Equality inference for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq2i 5068 
Equality inference for functions. (Contributed by NM, 5Sep2011.)



Theorem  feq23i 5069 
Equality inference for functions. (Contributed by Paul Chapman,
22Jun2011.)



Theorem  feq23d 5070 
Equality deduction for functions. (Contributed by NM, 8Jun2013.)



Theorem  nff 5071 
Boundvariable hypothesis builder for a mapping. (Contributed by NM,
29Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)



Theorem  sbcfng 5072* 
Distribute proper substitution through the function predicate with a
domain. (Contributed by Alexander van der Vekens, 15Jul2018.)



Theorem  sbcfg 5073* 
Distribute proper substitution through the function predicate with
domain and codomain. (Contributed by Alexander van der Vekens,
15Jul2018.)



Theorem  ffn 5074 
A mapping is a function. (Contributed by NM, 2Aug1994.)



Theorem  dffn2 5075 
Any function is a mapping into . (Contributed by NM, 31Oct1995.)
(Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  ffun 5076 
A mapping is a function. (Contributed by NM, 3Aug1994.)



Theorem  frel 5077 
A mapping is a relation. (Contributed by NM, 3Aug1994.)



Theorem  fdm 5078 
The domain of a mapping. (Contributed by NM, 2Aug1994.)



Theorem  fdmi 5079 
The domain of a mapping. (Contributed by NM, 28Jul2008.)



Theorem  frn 5080 
The range of a mapping. (Contributed by NM, 3Aug1994.)



Theorem  dffn3 5081 
A function maps to its range. (Contributed by NM, 1Sep1999.)



Theorem  fss 5082 
Expanding the codomain of a mapping. (Contributed by NM, 10May1998.)
(Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fssd 5083 
Expanding the codomain of a mapping, deduction form. (Contributed by
Glauco Siliprandi, 11Dec2019.)



Theorem  fco 5084 
Composition of two mappings. (Contributed by NM, 29Aug1999.) (Proof
shortened by Andrew Salmon, 17Sep2011.)



Theorem  fco2 5085 
Functionality of a composition with weakened out of domain condition on
the first argument. (Contributed by Stefan O'Rear, 11Mar2015.)



Theorem  fssxp 5086 
A mapping is a class of ordered pairs. (Contributed by NM, 3Aug1994.)
(Proof shortened by Andrew Salmon, 17Sep2011.)



Theorem  fex2 5087 
A function with bounded domain and range is a set. This version is proven
without the Axiom of Replacement. (Contributed by Mario Carneiro,
24Jun2015.)



Theorem  funssxp 5088 
Two ways of specifying a partial function from to .
(Contributed by NM, 13Nov2007.)



Theorem  ffdm 5089 
A mapping is a partial function. (Contributed by NM, 25Nov2007.)



Theorem  opelf 5090 
The members of an ordered pair element of a mapping belong to the
mapping's domain and codomain. (Contributed by NM, 10Dec2003.)
(Revised by Mario Carneiro, 26Apr2015.)



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



Theorem  fun2 5092 
The union of two functions with disjoint domains. (Contributed by Mario
Carneiro, 12Mar2015.)



Theorem  fnfco 5093 
Composition of two functions. (Contributed by NM, 22May2006.)



Theorem  fssres 5094 
Restriction of a function with a subclass of its domain. (Contributed by
NM, 23Sep2004.)



Theorem  fssres2 5095 
Restriction of a restricted function with a subclass of its domain.
(Contributed by NM, 21Jul2005.)



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



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



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



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

