Theorem List for Intuitionistic Logic Explorer - 5001-5100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | imain 5001 |
The image of an intersection is the intersection of images.
(Contributed by Paul Chapman, 11-Apr-2009.)
|
|
|
Theorem | funimaexglem 5002 |
Lemma for funimaexg 5003. It constitutes the interesting part of
funimaexg 5003, in which
. (Contributed by Jim
Kingdon,
27-Dec-2018.)
|
|
|
Theorem | funimaexg 5003 |
Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284.
Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM,
10-Sep-2006.)
|
|
|
Theorem | funimaex 5004 |
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, 17-Nov-2002.)
|
|
|
Theorem | isarep1 5005* |
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, 26-Oct-2006.) (Proof shortened by
Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | isarep2 5006* |
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 5004. (Contributed by NM, 26-Oct-2006.)
|
|
|
Theorem | fneq1 5007 |
Equality theorem for function predicate with domain. (Contributed by NM,
1-Aug-1994.)
|
|
|
Theorem | fneq2 5008 |
Equality theorem for function predicate with domain. (Contributed by NM,
1-Aug-1994.)
|
|
|
Theorem | fneq1d 5009 |
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | fneq2d 5010 |
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | fneq12d 5011 |
Equality deduction for function predicate with domain. (Contributed by
NM, 26-Jun-2011.)
|
|
|
Theorem | fneq12 5012 |
Equality theorem for function predicate with domain. (Contributed by
Thierry Arnoux, 31-Jan-2017.)
|
|
|
Theorem | fneq1i 5013 |
Equality inference for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | fneq2i 5014 |
Equality inference for function predicate with domain. (Contributed by
NM, 4-Sep-2011.)
|
|
|
Theorem | nffn 5015 |
Bound-variable hypothesis builder for a function with domain.
(Contributed by NM, 30-Jan-2004.)
|
|
|
Theorem | fnfun 5016 |
A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
|
|
|
Theorem | fnrel 5017 |
A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
|
|
|
Theorem | fndm 5018 |
The domain of a function. (Contributed by NM, 2-Aug-1994.)
|
|
|
Theorem | funfni 5019 |
Inference to convert a function and domain antecedent. (Contributed by
NM, 22-Apr-2004.)
|
|
|
Theorem | fndmu 5020 |
A function has a unique domain. (Contributed by NM, 11-Aug-1994.)
|
|
|
Theorem | fnbr 5021 |
The first argument of binary relation on a function belongs to the
function's domain. (Contributed by NM, 7-May-2004.)
|
|
|
Theorem | fnop 5022 |
The first argument of an ordered pair in a function belongs to the
function's domain. (Contributed by NM, 8-Aug-1994.)
|
|
|
Theorem | fneu 5023* |
There is exactly one value of a function. (Contributed by NM,
22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | fneu2 5024* |
There is exactly one value of a function. (Contributed by NM,
7-Nov-1995.)
|
|
|
Theorem | fnun 5025 |
The union of two functions with disjoint domains. (Contributed by NM,
22-Sep-2004.)
|
|
|
Theorem | fnunsn 5026 |
Extension of a function with a new ordered pair. (Contributed by NM,
28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | fnco 5027 |
Composition of two functions. (Contributed by NM, 22-May-2006.)
|
|
|
Theorem | fnresdm 5028 |
A function does not change when restricted to its domain. (Contributed by
NM, 5-Sep-2004.)
|
|
|
Theorem | fnresdisj 5029 |
A function restricted to a class disjoint with its domain is empty.
(Contributed by NM, 23-Sep-2004.)
|
|
|
Theorem | 2elresin 5030 |
Membership in two functions restricted by each other's domain.
(Contributed by NM, 8-Aug-1994.)
|
|
|
Theorem | fnssresb 5031 |
Restriction of a function with a subclass of its domain. (Contributed by
NM, 10-Oct-2007.)
|
|
|
Theorem | fnssres 5032 |
Restriction of a function with a subclass of its domain. (Contributed by
NM, 2-Aug-1994.)
|
|
|
Theorem | fnresin1 5033 |
Restriction of a function's domain with an intersection. (Contributed by
NM, 9-Aug-1994.)
|
|
|
Theorem | fnresin2 5034 |
Restriction of a function's domain with an intersection. (Contributed by
NM, 9-Aug-1994.)
|
|
|
Theorem | fnres 5035* |
An equivalence for functionality of a restriction. Compare dffun8 4949.
(Contributed by Mario Carneiro, 20-May-2015.)
|
|
|
Theorem | fnresi 5036 |
Functionality and domain of restricted identity. (Contributed by NM,
27-Aug-2004.)
|
|
|
Theorem | fnima 5037 |
The image of a function's domain is its range. (Contributed by NM,
4-Nov-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | fn0 5038 |
A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.)
(Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | fnimadisj 5039 |
A class that is disjoint with the domain of a function has an empty image
under the function. (Contributed by FL, 24-Jan-2007.)
|
|
|
Theorem | fnimaeq0 5040 |
Images under a function never map nonempty sets to empty sets.
(Contributed by Stefan O'Rear, 21-Jan-2015.)
|
|
|
Theorem | dfmpt3 5041 |
Alternate definition for the "maps to" notation df-mpt 3841. (Contributed
by Mario Carneiro, 30-Dec-2016.)
|
|
|
Theorem | fnopabg 5042* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro,
4-Dec-2016.)
|
|
|
Theorem | fnopab 5043* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 5-Mar-1996.)
|
|
|
Theorem | mptfng 5044* |
The maps-to notation defines a function with domain. (Contributed by
Scott Fenton, 21-Mar-2011.)
|
|
|
Theorem | fnmpt 5045* |
The maps-to notation defines a function with domain. (Contributed by
NM, 9-Apr-2013.)
|
|
|
Theorem | mpt0 5046 |
A mapping operation with empty domain. (Contributed by Mario Carneiro,
28-Dec-2014.)
|
|
|
Theorem | fnmpti 5047* |
Functionality and domain of an ordered-pair class abstraction.
(Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | dmmpti 5048* |
Domain of an ordered-pair class abstraction that specifies a function.
(Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
|
|
Theorem | mptun 5049 |
Union of mappings which are mutually compatible. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
|
|
Theorem | feq1 5050 |
Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
|
|
|
Theorem | feq2 5051 |
Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
|
|
|
Theorem | feq3 5052 |
Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
|
|
|
Theorem | feq23 5053 |
Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (Proof
shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | feq1d 5054 |
Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)
|
|
|
Theorem | feq2d 5055 |
Equality deduction for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
|
|
Theorem | feq12d 5056 |
Equality deduction for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
|
|
Theorem | feq123d 5057 |
Equality deduction for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
|
|
Theorem | feq123 5058 |
Equality theorem for functions. (Contributed by FL, 16-Nov-2008.)
|
|
|
Theorem | feq1i 5059 |
Equality inference for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
|
|
Theorem | feq2i 5060 |
Equality inference for functions. (Contributed by NM, 5-Sep-2011.)
|
|
|
Theorem | feq23i 5061 |
Equality inference for functions. (Contributed by Paul Chapman,
22-Jun-2011.)
|
|
|
Theorem | feq23d 5062 |
Equality deduction for functions. (Contributed by NM, 8-Jun-2013.)
|
|
|
Theorem | nff 5063 |
Bound-variable hypothesis builder for a mapping. (Contributed by NM,
29-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | sbcfng 5064* |
Distribute proper substitution through the function predicate with a
domain. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|
|
|
Theorem | sbcfg 5065* |
Distribute proper substitution through the function predicate with
domain and codomain. (Contributed by Alexander van der Vekens,
15-Jul-2018.)
|
|
|
Theorem | ffn 5066 |
A mapping is a function. (Contributed by NM, 2-Aug-1994.)
|
|
|
Theorem | dffn2 5067 |
Any function is a mapping into . (Contributed by NM, 31-Oct-1995.)
(Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | ffun 5068 |
A mapping is a function. (Contributed by NM, 3-Aug-1994.)
|
|
|
Theorem | frel 5069 |
A mapping is a relation. (Contributed by NM, 3-Aug-1994.)
|
|
|
Theorem | fdm 5070 |
The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
|
|
|
Theorem | fdmi 5071 |
The domain of a mapping. (Contributed by NM, 28-Jul-2008.)
|
|
|
Theorem | frn 5072 |
The range of a mapping. (Contributed by NM, 3-Aug-1994.)
|
|
|
Theorem | dffn3 5073 |
A function maps to its range. (Contributed by NM, 1-Sep-1999.)
|
|
|
Theorem | fss 5074 |
Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.)
(Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | fssd 5075 |
Expanding the codomain of a mapping, deduction form. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | fco 5076 |
Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof
shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | fco2 5077 |
Functionality of a composition with weakened out of domain condition on
the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015.)
|
|
|
Theorem | fssxp 5078 |
A mapping is a class of ordered pairs. (Contributed by NM, 3-Aug-1994.)
(Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | fex2 5079 |
A function with bounded domain and range is a set. This version is proven
without the Axiom of Replacement. (Contributed by Mario Carneiro,
24-Jun-2015.)
|
|
|
Theorem | funssxp 5080 |
Two ways of specifying a partial function from to .
(Contributed by NM, 13-Nov-2007.)
|
|
|
Theorem | ffdm 5081 |
A mapping is a partial function. (Contributed by NM, 25-Nov-2007.)
|
|
|
Theorem | opelf 5082 |
The members of an ordered pair element of a mapping belong to the
mapping's domain and codomain. (Contributed by NM, 10-Dec-2003.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | fun 5083 |
The union of two functions with disjoint domains. (Contributed by NM,
22-Sep-2004.)
|
|
|
Theorem | fun2 5084 |
The union of two functions with disjoint domains. (Contributed by Mario
Carneiro, 12-Mar-2015.)
|
|
|
Theorem | fnfco 5085 |
Composition of two functions. (Contributed by NM, 22-May-2006.)
|
|
|
Theorem | fssres 5086 |
Restriction of a function with a subclass of its domain. (Contributed by
NM, 23-Sep-2004.)
|
|
|
Theorem | fssres2 5087 |
Restriction of a restricted function with a subclass of its domain.
(Contributed by NM, 21-Jul-2005.)
|
|
|
Theorem | fresin 5088 |
An identity for the mapping relationship under restriction. (Contributed
by Scott Fenton, 4-Sep-2011.) (Proof shortened by Mario Carneiro,
26-May-2016.)
|
|
|
Theorem | resasplitss 5089 |
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, 28-Dec-2018.)
|
|
|
Theorem | fcoi1 5090 |
Composition of a mapping and restricted identity. (Contributed by NM,
13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | fcoi2 5091 |
Composition of restricted identity and a mapping. (Contributed by NM,
13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | feu 5092* |
There is exactly one value of a function in its codomain. (Contributed
by NM, 10-Dec-2003.)
|
|
|
Theorem | fcnvres 5093 |
The converse of a restriction of a function. (Contributed by NM,
26-Mar-1998.)
|
|
|
Theorem | fimacnvdisj 5094 |
The preimage of a class disjoint with a mapping's codomain is empty.
(Contributed by FL, 24-Jan-2007.)
|
|
|
Theorem | fintm 5095* |
Function into an intersection. (Contributed by Jim Kingdon,
28-Dec-2018.)
|
|
|
Theorem | fin 5096 |
Mapping into an intersection. (Contributed by NM, 14-Sep-1999.) (Proof
shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | fabexg 5097* |
Existence of a set of functions. (Contributed by Paul Chapman,
25-Feb-2008.)
|
|
|
Theorem | fabex 5098* |
Existence of a set of functions. (Contributed by NM, 3-Dec-2007.)
|
|
|
Theorem | dmfex 5099 |
If a mapping is a set, its domain is a set. (Contributed by NM,
27-Aug-2006.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | f0 5100 |
The empty function. (Contributed by NM, 14-Aug-1999.)
|
|