Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  funimaexg 4926 
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 4927 
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 4928* 
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 4929* 
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 4927. (Contributed by NM,
26Oct2006.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

