Home | Metamath
Proof Explorer Theorem List (p. 60 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dffun5 5901* | Alternate definition of function. (Contributed by NM, 29-Dec-1996.) |
Theorem | dffun6f 5902* | Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | dffun6 5903* | Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) |
Theorem | funmo 5904* | A function has at most one value for each argument. (Contributed by NM, 24-May-1998.) |
Theorem | funrel 5905 | A function is a relation. (Contributed by NM, 1-Aug-1994.) |
Theorem | 0nelfun 5906 | A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021.) |
Theorem | funss 5907 | Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) |
Theorem | funeq 5908 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
Theorem | funeqi 5909 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | funeqd 5910 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
Theorem | nffun 5911 | Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.) |
Theorem | sbcfung 5912 | Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
Theorem | funeu 5913* | There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | funeu2 5914* | There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.) |
Theorem | dffun7 5915* | 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 5916 shows that it doesn't matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.) |
Theorem | dffun8 5916* | Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 5915. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | dffun9 5917* | Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
Theorem | funfn 5918 | An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.) |
Theorem | funfnd 5919 | A function is a function over its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Theorem | funi 5920 | The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. (Contributed by NM, 30-Apr-1998.) |
Theorem | nfunv 5921 | The universe is not a function. (Contributed by Raph Levien, 27-Jan-2004.) |
Theorem | funopg 5922 | A Kuratowski ordered pair is a function only if its components are equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
Theorem | funopab 5923* | A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995.) |
Theorem | funopabeq 5924* | A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.) |
Theorem | funopab4 5925* | A class of ordered pairs of values in the form used by df-mpt 4730 is a function. (Contributed by NM, 17-Feb-2013.) |
Theorem | funmpt 5926 | A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.) |
Theorem | funmpt2 5927 | Functionality of a class given by a "maps to" notation. (Contributed by FL, 17-Feb-2008.) (Revised by Mario Carneiro, 31-May-2014.) |
Theorem | funco 5928 | The composition of two functions is a function. Exercise 29 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | funres 5929 | A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.) |
Theorem | funssres 5930 | The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.) |
Theorem | fun2ssres 5931 | Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994.) |
Theorem | funun 5932 | The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by NM, 12-Aug-1994.) |
Theorem | fununmo 5933* | If the union of classes is a function, there is at most one element in relation to an arbitrary element regarding one of these classes. (Contributed by AV, 18-Jul-2019.) |
Theorem | fununfun 5934 | If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019.) |
Theorem | fundif 5935 | A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021.) |
Theorem | funcnvsn 5936 | The converse singleton of an ordered pair is a function. This is equivalent to funsn 5939 via cnvsn 5618, but stating it this way allows us to skip the sethood assumptions on and . (Contributed by NM, 30-Apr-2015.) |
Theorem | funsng 5937 | A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 28-Jun-2011.) |
Theorem | fnsng 5938 | Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.) |
Theorem | funsn 5939 | A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 12-Aug-1994.) |
Theorem | funprg 5940 | A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.) |
Theorem | funprgOLD 5941 | Obsolete proof of funprg 5940 as of 14-Jul-2021. (Contributed by FL, 26-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | funtpg 5942 | A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Proof shortened by JJ, 14-Jul-2021.) |
Theorem | funtpgOLD 5943 | Obsolete proof of funtpg 5942 as of 14-Jul-2021. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | funpr 5944 | A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
Theorem | funtp 5945 | A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
Theorem | fnsn 5946 | Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | fnprg 5947 | Function with a domain of two different values. (Contributed by FL, 26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | fntpg 5948 | Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017.) |
Theorem | fntp 5949 | A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | funcnvpr 5950 | The converse pair of ordered pairs is a function if the second members are different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021.) |
Theorem | funcnvtp 5951 | The converse triple of ordered pairs is a function if the second members are pairwise different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021.) |
Theorem | funcnvqp 5952 | The converse quadruple of ordered pairs is a function if the second members are pairwise different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021.) (Proof shortened by JJ, 14-Jul-2021.) |
Theorem | funcnvqpOLD 5953 | Obsolete proof of funcnvqp 5952 as of 14-Jul-2021. (Contributed by AV, 23-Jan-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | fun0 5954 | The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by NM, 7-Apr-1998.) |
Theorem | funcnv0 5955 | The converse of the empty set is a function. (Contributed by AV, 7-Jan-2021.) |
Theorem | funcnvcnv 5956 | The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.) |
Theorem | funcnv2 5957* | A simpler equivalence for single-rooted (see funcnv 5958). (Contributed by NM, 9-Aug-2004.) |
Theorem | funcnv 5958* | The converse of a class is a function iff the class is single-rooted, which means that for any in the range of there is at most one such that . Definition of single-rooted in [Enderton] p. 43. See funcnv2 5957 for a simpler version. (Contributed by NM, 13-Aug-2004.) |
Theorem | funcnv3 5959* | A condition showing a class is single-rooted. (See funcnv 5958). (Contributed by NM, 26-May-2006.) |
Theorem | fun2cnv 5960* | The double converse of a class is a function iff the class is single-valued. Each side is equivalent to Definition 6.4(2) of [TakeutiZaring] p. 23, who use the notation "Un(A)" for single-valued. Note that is not necessarily a function. (Contributed by NM, 13-Aug-2004.) |
Theorem | svrelfun 5961 | A single-valued relation is a function. (See fun2cnv 5960 for "single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 17-Jan-2006.) |
Theorem | fncnv 5962* | Single-rootedness (see funcnv 5958) of a class cut down by a Cartesian product. (Contributed by NM, 5-Mar-2007.) |
Theorem | fun11 5963* | Two ways of stating that is one-to-one (but not necessarily a function). Each side is equivalent to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation "Un2 (A)" for one-to-one (but not necessarily a function). (Contributed by NM, 17-Jan-2006.) |
Theorem | fununi 5964* | The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.) |
Theorem | funin 5965 | The intersection with a function is a function. Exercise 14(a) of [Enderton] p. 53. (Contributed by NM, 19-Mar-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | funres11 5966 | The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998.) |
Theorem | funcnvres 5967 | The converse of a restricted function. (Contributed by NM, 27-Mar-1998.) |
Theorem | cnvresid 5968 | Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.) |
Theorem | funcnvres2 5969 | The converse of a restriction of the converse of a function equals the function restricted to the image of its converse. (Contributed by NM, 4-May-2005.) |
Theorem | funimacnv 5970 | The image of the preimage of a function. (Contributed by NM, 25-May-2004.) |
Theorem | funimass1 5971 | A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by NM, 25-May-2004.) |
Theorem | funimass2 5972 | A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by NM, 25-May-2004.) |
Theorem | imadif 5973 | The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.) |
Theorem | imain 5974 | The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.) |
Theorem | funimaexg 5975 | 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 5976 | The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep 4771. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 17-Nov-2002.) |
Theorem | isarep1 5977* | 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 5978* | 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 5976. (Contributed by NM, 26-Oct-2006.) |
Theorem | fneq1 5979 | Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.) |
Theorem | fneq2 5980 | Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.) |
Theorem | fneq1d 5981 | Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | fneq2d 5982 | Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | fneq12d 5983 | Equality deduction for function predicate with domain. (Contributed by NM, 26-Jun-2011.) |
Theorem | fneq12 5984 | Equality theorem for function predicate with domain. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
Theorem | fneq1i 5985 | Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | fneq2i 5986 | Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.) |
Theorem | nffn 5987 | Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.) |
Theorem | fnfun 5988 | A function with domain is a function. (Contributed by NM, 1-Aug-1994.) |
Theorem | fnrel 5989 | A function with domain is a relation. (Contributed by NM, 1-Aug-1994.) |
Theorem | fndm 5990 | The domain of a function. (Contributed by NM, 2-Aug-1994.) |
Theorem | funfni 5991 | Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.) |
Theorem | fndmu 5992 | A function has a unique domain. (Contributed by NM, 11-Aug-1994.) |
Theorem | fnbr 5993 | The first argument of binary relation on a function belongs to the function's domain. (Contributed by NM, 7-May-2004.) |
Theorem | fnop 5994 | The first argument of an ordered pair in a function belongs to the function's domain. (Contributed by NM, 8-Aug-1994.) |
Theorem | fneu 5995* | There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | fneu2 5996* | There is exactly one value of a function. (Contributed by NM, 7-Nov-1995.) |
Theorem | fnun 5997 | The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.) |
Theorem | fnunsn 5998 | Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | fnco 5999 | Composition of two functions. (Contributed by NM, 22-May-2006.) |
Theorem | fnresdm 6000 | A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |