Home | Intuitionistic Logic Explorer Theorem List (p. 40 of 94) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elpw2g 3901 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
Theorem | elpw2 3902 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
Theorem | pwnss 3903 | The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Theorem | pwne 3904 | No set equals its power set. The sethood antecedent is necessary; compare pwv 3570. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
Theorem | repizf2lem 3905 | Lemma for repizf2 3906. If we have a function-like proposition which provides at most one value of for each in a set , we can change "at most one" to "exactly one" by restricting the values of to those values for which the proposition provides a value of . (Contributed by Jim Kingdon, 7-Sep-2018.) |
Theorem | repizf2 3906* | Replacement. This version of replacement is stronger than repizf 3864 in the sense that does not need to map all values of in to a value of . The resulting set contains those elements for which there is a value of and in that sense, this theorem combines repizf 3864 with ax-sep 3866. Another variation would be but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.) |
Theorem | class2seteq 3907* | Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |
Theorem | 0elpw 3908 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
Theorem | 0nep0 3909 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |
Theorem | 0inp0 3910 | Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 30-Sep-2003.) |
Theorem | unidif0 3911 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |
Theorem | iin0imm 3912* | An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
Theorem | iin0r 3913* | If an indexed intersection of the empty set is empty, the index set is non-empty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
Theorem | intv 3914 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |
Theorem | axpweq 3915* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 3918 is not used by the proof. (Contributed by NM, 22-Jun-2009.) |
Theorem | bnd 3916* | A very strong generalization of the Axiom of Replacement (compare zfrep6 3865). Its strength lies in the rather profound fact that does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom. In the context of IZF, it is just a slight variation of ax-coll 3863. (Contributed by NM, 17-Oct-2004.) |
Theorem | bnd2 3917* | A variant of the Boundedness Axiom bnd 3916 that picks a subset out of a possibly proper class in which a property is true. (Contributed by NM, 4-Feb-2004.) |
Axiom | ax-pow 3918* |
Axiom of Power Sets. An axiom of Intuitionistic Zermelo-Fraenkel set
theory. It states that a set exists that includes the power set
of a given set
i.e. contains every subset of . This is
Axiom 8 of [Crosilla] p. "Axioms
of CZF and IZF" except (a) unnecessary
quantifiers are removed, and (b) Crosilla has a biconditional rather
than an implication (but the two are equivalent by bm1.3ii 3869).
The variant axpow2 3920 uses explicit subset notation. A version using class notation is pwex 3923. (Contributed by NM, 5-Aug-1993.) |
Theorem | zfpow 3919* | Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
Theorem | axpow2 3920* | A variant of the Axiom of Power Sets ax-pow 3918 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
Theorem | axpow3 3921* | A variant of the Axiom of Power Sets ax-pow 3918. For any set , there exists a set whose members are exactly the subsets of i.e. the power set of . Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
Theorem | el 3922* | Every set is an element of some other set. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | pwex 3923 | Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | pwexg 3924 | Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) |
Theorem | abssexg 3925* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | snexgOLD 3926 | A singleton whose element exists is a set. The case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. This is a special case of snexg 3927 and new proofs should use snexg 3927 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of snexg 3927 and then remove it. |
Theorem | snexg 3927 | A singleton whose element exists is a set. The case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.) |
Theorem | snex 3928 | A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | snexprc 3929 | A singleton whose element is a proper class is a set. The case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.) |
Theorem | p0ex 3930 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |
Theorem | pp0ex 3931 | (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |
Theorem | ord3ex 3932 | The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.) |
Theorem | dtruarb 3933* | At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). This theorem asserts the existence of two sets which do not equal each other; compare with dtruex 4237 in which we are given a set and go from there to a set which is not equal to it. (Contributed by Jim Kingdon, 2-Sep-2018.) |
Theorem | pwuni 3934 | A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) |
Axiom | ax-pr 3935* | The Axiom of Pairing of IZF set theory. Axiom 2 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 3869). (Contributed by NM, 14-Nov-2006.) |
Theorem | zfpair2 3936 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 3935. (Contributed by NM, 14-Nov-2006.) |
Theorem | prexgOLD 3937 | The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3471, prprc1 3469, and prprc2 3470. This is a special case of prexg 3938 and new proofs should use prexg 3938 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of prexg 3938 and then remove it. |
Theorem | prexg 3938 | The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3471, prprc1 3469, and prprc2 3470. (Contributed by Jim Kingdon, 16-Sep-2018.) |
Theorem | snelpwi 3939 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.) |
Theorem | snelpw 3940 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |
Theorem | prelpwi 3941 | A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.) |
Theorem | rext 3942* | A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.) |
Theorem | sspwb 3943 | Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
Theorem | unipw 3944 | A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.) |
Theorem | pwel 3945 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |
Theorem | pwtr 3946 | A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.) |
Theorem | ssextss 3947* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
Theorem | ssext 3948* | An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets. (Contributed by NM, 30-Jun-2004.) |
Theorem | nssssr 3949* | Negation of subclass relationship. Compare nssr 2997. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | pweqb 3950 | Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
Theorem | intid 3951* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |
Theorem | euabex 3952 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
Theorem | mss 3953* | An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | exss 3954* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
Theorem | opexg 3955 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
Theorem | opexgOLD 3956 | An ordered pair of sets is a set. This is a special case of opexg 3955 and new proofs should use opexg 3955 instead. (Contributed by Jim Kingdon, 19-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of opexg 3955 and then remove it. |
Theorem | opex 3957 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | otexg 3958 | An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.) |
Theorem | elop 3959 | An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opi1 3960 | One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opi2 3961 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opm 3962* | An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.) |
Theorem | opnzi 3963 | An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3962). (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth1 3964 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth 3965 | The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that and are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.) |
Theorem | opthg 3966 | Ordered pair theorem. and are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opthg2 3967 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth2 3968 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
Theorem | otth2 3969 | Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | otth 3970 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | eqvinop 3971* | A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
Theorem | copsexg 3972* | Substitution of class for ordered pair . (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | copsex2t 3973* | Closed theorem form of copsex2g 3974. (Contributed by NM, 17-Feb-2013.) |
Theorem | copsex2g 3974* | Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) |
Theorem | copsex4g 3975* | An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.) |
Theorem | 0nelop 3976 | A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opeqex 3977 | Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.) |
Theorem | opcom 3978 | An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.) |
Theorem | moop2 3979* | "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opeqsn 3980 | Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) |
Theorem | opeqpr 3981 | Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) |
Theorem | euotd 3982* | Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.) |
Theorem | uniop 3983 | The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | uniopel 3984 | Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opabid 3985 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | elopab 3986* | Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.) |
Theorem | opelopabsbALT 3987* | The law of concretion in terms of substitutions. Less general than opelopabsb 3988, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | opelopabsb 3988* | The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
Theorem | brabsb 3989* | The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.) |
Theorem | opelopabt 3990* | Closed theorem form of opelopab 3999. (Contributed by NM, 19-Feb-2013.) |
Theorem | opelopabga 3991* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | brabga 3992* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab2a 3993* | Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopaba 3994* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | braba 3995* | The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.) |
Theorem | opelopabg 3996* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | brabg 3997* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab2 3998* | Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab 3999* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.) |
Theorem | brab 4000* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |