Type  Label  Description 
Statement 

Syntax  wf1o 4901 
Extend the definition of a wff to include onetoone onto functions.
(Read: maps onetoone onto .) The notation
("11"
above the arrow and "onto" below the arrow) is from Definition
6.15(6) of
[TakeutiZaring] p. 27.



Syntax  cfv 4902 
Extend the definition of a class to include the value of a function.
(Read: The value of at , or
" of .")



Syntax  wiso 4903 
Extend the definition of a wff to include the isomorphism property.
(Read: is an
, isomorphism of onto .)



Definition  dffun 4904 
Define predicate that determines if some class is a function.
Definition 10.1 of [Quine] p. 65. For
example, the expression
is true (funi 4932). This is not the same as defining a
specific function's mapping, which is typically done using the format of
cmpt 3818 with the mapsto notation (see dfmpt 3820). Contrast this
predicate with the predicates to determine if some class is a function
with a given domain (dffn 4905), a function with a given domain and
codomain (dff 4906), a onetoone function (dff1 4907), an onto function
(dffo 4908), or a onetoone onto function (dff1o 4909). For alternate
definitions, see dffun2 4912, dffun4 4913, dffun6 4916, dffun7 4928, dffun8 4929,
and dffun9 4930. (Contributed by NM, 1Aug1994.)



Definition  dffn 4905 
Define a function with domain. Definition 6.15(1) of [TakeutiZaring]
p. 27. (Contributed by NM, 1Aug1994.)



Definition  dff 4906 
Define a function (mapping) with domain and codomain. Definition
6.15(3) of [TakeutiZaring] p. 27.
(Contributed by NM, 1Aug1994.)



Definition  dff1 4907 
Define a onetoone function. Compare Definition 6.15(5) of
[TakeutiZaring] p. 27. We use
their notation ("11" above the arrow).
(Contributed by NM, 1Aug1994.)



Definition  dffo 4908 
Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27.
We use their notation ("onto" under the arrow). (Contributed
by NM,
1Aug1994.)



Definition  dff1o 4909 
Define a onetoone onto function. Compare Definition 6.15(6) of
[TakeutiZaring] p. 27. We use
their notation ("11" above the arrow and
"onto" below the arrow). (Contributed by NM, 1Aug1994.)



Definition  dffv 4910* 
Define the value of a function, , also known as function
application. For example, . Typically,
function is
defined using mapsto notation (see dfmpt 3820), but
this is not required. For example, F = { 2 , 6 ,
3 , 9 } > ( F 3 ) = 9 . We will later define
twoargument functions using ordered pairs as
. This
particular definition is
quite convenient: it can be applied to any class and evaluates to the
empty set when it is not meaningful. The left apostrophe notation
originated with Peano and was adopted in Definition *30.01 of
[WhiteheadRussell] p. 235,
Definition 10.11 of [Quine] p. 68, and
Definition 6.11 of [TakeutiZaring]
p. 26. It means the same thing as
the more familiar notation for a function's value at ,
i.e. " of
," but without
contextdependent notational
ambiguity. (Contributed by NM, 1Aug1994.) Revised to use .
(Revised by Scott Fenton, 6Oct2017.)



Definition  dfisom 4911* 
Define the isomorphism predicate. We read this as " is an ,
isomorphism of
onto ." Normally, and are
ordering relations on and
respectively. Definition 6.28 of
[TakeutiZaring] p. 32, whose
notation is the same as ours except that
and are subscripts.
(Contributed by NM, 4Mar1997.)



Theorem  dffun2 4912* 
Alternate definition of a function. (Contributed by NM,
29Dec1996.)



Theorem  dffun4 4913* 
Alternate definition of a function. Definition 6.4(4) of
[TakeutiZaring] p. 24.
(Contributed by NM, 29Dec1996.)



Theorem  dffun5r 4914* 
A way of proving a relation is a function, analogous to mo2r 1952.
(Contributed by Jim Kingdon, 27May2020.)



Theorem  dffun6f 4915* 
Definition of function, using boundvariable hypotheses instead of
distinct variable conditions. (Contributed by NM, 9Mar1995.)
(Revised by Mario Carneiro, 15Oct2016.)



Theorem  dffun6 4916* 
Alternate definition of a function using "at most one" notation.
(Contributed by NM, 9Mar1995.)



Theorem  funmo 4917* 
A function has at most one value for each argument. (Contributed by NM,
24May1998.)



Theorem  dffun4f 4918* 
Definition of function like dffun4 4913 but using boundvariable hypotheses
instead of distinct variable conditions. (Contributed by Jim Kingdon,
17Mar2019.)



Theorem  funrel 4919 
A function is a relation. (Contributed by NM, 1Aug1994.)



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



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



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



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



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



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



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



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



Theorem  dffun7 4928* 
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 4929 shows that it doesn't matter
which meaning we pick.) (Contributed by NM, 4Nov2002.)



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



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



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



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



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



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



Theorem  funopab 4935* 
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 4936* 
A class of ordered pairs of values is a function. (Contributed by NM,
14Nov1995.)



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



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



Theorem  funmpt2 4939 
Functionality of a class given by a "maps to" notation. (Contributed
by
FL, 17Feb2008.) (Revised by Mario Carneiro, 31May2014.)



Theorem  funco 4940 
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 4941 
A restriction of a function is a function. Compare Exercise 18 of
[TakeutiZaring] p. 25. (Contributed
by NM, 16Aug1994.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  funimaexg 4983 
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 4984 
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 4985* 
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 4986* 
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 4984. (Contributed by NM, 26Oct2006.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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

