Home Intuitionistic Logic ExplorerTheorem List (p. 51 of 106) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 5001-5100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcnvresid 5001 Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.)

Theoremfuncnvres2 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, 4-May-2005.)

Theoremfunimacnv 5003 The image of the preimage of a function. (Contributed by NM, 25-May-2004.)

Theoremfunimass1 5004 A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by NM, 25-May-2004.)

Theoremfunimass2 5005 A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by NM, 25-May-2004.)

Theoremimadiflem 5006 One direction of imadif 5007. This direction does not require . (Contributed by Jim Kingdon, 25-Dec-2018.)

Theoremimadif 5007 The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)

Theoremimainlem 5008 One direction of imain 5009. This direction does not require . (Contributed by Jim Kingdon, 25-Dec-2018.)

Theoremimain 5009 The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)

Theoremfunimaexglem 5010 Lemma for funimaexg 5011. It constitutes the interesting part of funimaexg 5011, in which . (Contributed by Jim Kingdon, 27-Dec-2018.)

Theoremfunimaexg 5011 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.)

Theoremfunimaex 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, 17-Nov-2002.)

Theoremisarep1 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, 26-Oct-2006.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)

Theoremisarep2 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, 26-Oct-2006.)

Theoremfneq1 5015 Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)

Theoremfneq2 5016 Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)

Theoremfneq1d 5017 Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremfneq2d 5018 Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremfneq12d 5019 Equality deduction for function predicate with domain. (Contributed by NM, 26-Jun-2011.)

Theoremfneq12 5020 Equality theorem for function predicate with domain. (Contributed by Thierry Arnoux, 31-Jan-2017.)

Theoremfneq1i 5021 Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremfneq2i 5022 Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)

Theoremnffn 5023 Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)

Theoremfnfun 5024 A function with domain is a function. (Contributed by NM, 1-Aug-1994.)

Theoremfnrel 5025 A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)

Theoremfndm 5026 The domain of a function. (Contributed by NM, 2-Aug-1994.)

Theoremfunfni 5027 Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)

Theoremfndmu 5028 A function has a unique domain. (Contributed by NM, 11-Aug-1994.)

Theoremfnbr 5029 The first argument of binary relation on a function belongs to the function's domain. (Contributed by NM, 7-May-2004.)

Theoremfnop 5030 The first argument of an ordered pair in a function belongs to the function's domain. (Contributed by NM, 8-Aug-1994.)

Theoremfneu 5031* There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremfneu2 5032* There is exactly one value of a function. (Contributed by NM, 7-Nov-1995.)

Theoremfnun 5033 The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)

Theoremfnunsn 5034 Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)

Theoremfnco 5035 Composition of two functions. (Contributed by NM, 22-May-2006.)

Theoremfnresdm 5036 A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)

Theoremfnresdisj 5037 A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004.)

Theorem2elresin 5038 Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994.)

Theoremfnssresb 5039 Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007.)

Theoremfnssres 5040 Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)

Theoremfnresin1 5041 Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.)

Theoremfnresin2 5042 Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.)

Theoremfnres 5043* An equivalence for functionality of a restriction. Compare dffun8 4957. (Contributed by Mario Carneiro, 20-May-2015.)

Theoremfnresi 5044 Functionality and domain of restricted identity. (Contributed by NM, 27-Aug-2004.)

Theoremfnima 5045 The image of a function's domain is its range. (Contributed by NM, 4-Nov-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremfn0 5046 A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremfnimadisj 5047 A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007.)

Theoremfnimaeq0 5048 Images under a function never map nonempty sets to empty sets. (Contributed by Stefan O'Rear, 21-Jan-2015.)

Theoremdfmpt3 5049 Alternate definition for the "maps to" notation df-mpt 3848. (Contributed by Mario Carneiro, 30-Dec-2016.)

Theoremfnopabg 5050* Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)

Theoremfnopab 5051* Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 5-Mar-1996.)

Theoremmptfng 5052* The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.)

Theoremfnmpt 5053* The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.)

Theoremmpt0 5054 A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.)

Theoremfnmpti 5055* Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)

Theoremdmmpti 5056* Domain of an ordered-pair class abstraction that specifies a function. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.)

Theoremmptun 5057 Union of mappings which are mutually compatible. (Contributed by Mario Carneiro, 31-Aug-2015.)

Theoremfeq1 5058 Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Theoremfeq2 5059 Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Theoremfeq3 5060 Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Theoremfeq23 5061 Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremfeq1d 5062 Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)

Theoremfeq2d 5063 Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremfeq12d 5064 Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremfeq123d 5065 Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremfeq123 5066 Equality theorem for functions. (Contributed by FL, 16-Nov-2008.)

Theoremfeq1i 5067 Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremfeq2i 5068 Equality inference for functions. (Contributed by NM, 5-Sep-2011.)

Theoremfeq23i 5069 Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremfeq23d 5070 Equality deduction for functions. (Contributed by NM, 8-Jun-2013.)

Theoremnff 5071 Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)

Theoremsbcfng 5072* Distribute proper substitution through the function predicate with a domain. (Contributed by Alexander van der Vekens, 15-Jul-2018.)

Theoremsbcfg 5073* Distribute proper substitution through the function predicate with domain and codomain. (Contributed by Alexander van der Vekens, 15-Jul-2018.)

Theoremffn 5074 A mapping is a function. (Contributed by NM, 2-Aug-1994.)

Theoremdffn2 5075 Any function is a mapping into . (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremffun 5076 A mapping is a function. (Contributed by NM, 3-Aug-1994.)

Theoremfrel 5077 A mapping is a relation. (Contributed by NM, 3-Aug-1994.)

Theoremfdm 5078 The domain of a mapping. (Contributed by NM, 2-Aug-1994.)

Theoremfdmi 5079 The domain of a mapping. (Contributed by NM, 28-Jul-2008.)

Theoremfrn 5080 The range of a mapping. (Contributed by NM, 3-Aug-1994.)

Theoremdffn3 5081 A function maps to its range. (Contributed by NM, 1-Sep-1999.)

Theoremfss 5082 Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremfssd 5083 Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Theoremfco 5084 Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremfco2 5085 Functionality of a composition with weakened out of domain condition on the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015.)

Theoremfssxp 5086 A mapping is a class of ordered pairs. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremfex2 5087 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.)

Theoremfunssxp 5088 Two ways of specifying a partial function from to . (Contributed by NM, 13-Nov-2007.)

Theoremffdm 5089 A mapping is a partial function. (Contributed by NM, 25-Nov-2007.)

Theoremopelf 5090 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.)

Theoremfun 5091 The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)

Theoremfun2 5092 The union of two functions with disjoint domains. (Contributed by Mario Carneiro, 12-Mar-2015.)

Theoremfnfco 5093 Composition of two functions. (Contributed by NM, 22-May-2006.)

Theoremfssres 5094 Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.)

Theoremfssres2 5095 Restriction of a restricted function with a subclass of its domain. (Contributed by NM, 21-Jul-2005.)

Theoremfresin 5096 An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 26-May-2016.)

Theoremresasplitss 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, 28-Dec-2018.)

Theoremfcoi1 5098 Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremfcoi2 5099 Composition of restricted identity and a mapping. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Theoremfeu 5100* There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10511
 Copyright terms: Public domain < Previous  Next >