Home | Intuitionistic Logic Explorer Theorem List (p. 40 of 108) | < 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 | ax9vsep 3901* | Derive a weakened version of ax-9 1464, where and must be distinct, from Separation ax-sep 3896 and Extensionality ax-ext 2063. In intuitionistic logic a9evsep 3900 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | zfnuleu 3902* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2066 to strengthen the hypothesis in the form of axnul 3903). (Contributed by NM, 22-Dec-2007.) |
Theorem | axnul 3903* |
The Null Set Axiom of ZF set theory: there exists a set with no
elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks,
this is presented as a separate axiom; here we show it can be derived
from Separation ax-sep 3896. This version of the Null Set Axiom tells us
that at least one empty set exists, but does not tell us that it is
unique - we need the Axiom of Extensionality to do that (see
zfnuleu 3902).
This theorem should not be referenced by any proof. Instead, use ax-nul 3904 below so that the uses of the Null Set Axiom can be more easily identified. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Revised by NM, 4-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
Axiom | ax-nul 3904* | The Null Set Axiom of IZF set theory. It was derived as axnul 3903 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. Axiom 4 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by NM, 7-Aug-2003.) |
Theorem | 0ex 3905 | The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 3904. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | csbexga 3906 | The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Theorem | csbexa 3907 | The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | nalset 3908* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |
Theorem | vprc 3909 | The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity. (Contributed by NM, 23-Aug-1993.) |
Theorem | nvel 3910 | The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.) |
Theorem | vnex 3911 | The universal class does not exist. (Contributed by NM, 4-Jul-2005.) |
Theorem | inex1 3912 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
Theorem | inex2 3913 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |
Theorem | inex1g 3914 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
Theorem | ssex 3915 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 3896 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |
Theorem | ssexi 3916 | The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
Theorem | ssexg 3917 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
Theorem | ssexd 3918 | A subclass of a set is a set. Deduction form of ssexg 3917. (Contributed by David Moews, 1-May-2017.) |
Theorem | difexg 3919 | Existence of a difference. (Contributed by NM, 26-May-1998.) |
Theorem | zfausab 3920* | Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) |
Theorem | rabexg 3921* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) |
Theorem | rabex 3922* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.) |
Theorem | elssabg 3923* | Membership in a class abstraction involving a subset. Unlike elabg 2739, does not have to be a set. (Contributed by NM, 29-Aug-2006.) |
Theorem | inteximm 3924* | The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intexr 3925 | If the intersection of a class exists, the class is non-empty. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intnexr 3926 | If a class intersection is the universe, it is not a set. In classical logic this would be an equivalence. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intexabim 3927 | The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intexrabim 3928 | The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | iinexgm 3929* | The existence of an indexed union. is normally a free-variable parameter in , which should be read . (Contributed by Jim Kingdon, 28-Aug-2018.) |
Theorem | inuni 3930* | The intersection of a union with a class is equal to the union of the intersections of each element of with . (Contributed by FL, 24-Mar-2007.) |
Theorem | elpw2g 3931 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
Theorem | elpw2 3932 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
Theorem | pwnss 3933 | The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Theorem | pwne 3934 | No set equals its power set. The sethood antecedent is necessary; compare pwv 3600. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
Theorem | repizf2lem 3935 | Lemma for repizf2 3936. 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 3936* | Replacement. This version of replacement is stronger than repizf 3894 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 3894 with ax-sep 3896. Another variation would be but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.) |
Theorem | class2seteq 3937* | Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |
Theorem | 0elpw 3938 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
Theorem | 0nep0 3939 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |
Theorem | 0inp0 3940 | 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 3941 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |
Theorem | iin0imm 3942* | An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
Theorem | iin0r 3943* | 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 3944 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |
Theorem | axpweq 3945* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 3948 is not used by the proof. (Contributed by NM, 22-Jun-2009.) |
Theorem | bnd 3946* | A very strong generalization of the Axiom of Replacement (compare zfrep6 3895). 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 3893. (Contributed by NM, 17-Oct-2004.) |
Theorem | bnd2 3947* | A variant of the Boundedness Axiom bnd 3946 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 3948* |
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 3899).
The variant axpow2 3950 uses explicit subset notation. A version using class notation is pwex 3953. (Contributed by NM, 5-Aug-1993.) |
Theorem | zfpow 3949* | Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
Theorem | axpow2 3950* | A variant of the Axiom of Power Sets ax-pow 3948 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
Theorem | axpow3 3951* | A variant of the Axiom of Power Sets ax-pow 3948. 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 3952* | 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 3953 | 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 3954 | 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 3955* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | snexg 3956 | 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 3957 | A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | snexprc 3958 | 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 3959 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |
Theorem | pp0ex 3960 | (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |
Theorem | ord3ex 3961 | The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.) |
Theorem | dtruarb 3962* | 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 4302 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 3963 | 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 3964* | 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 3899). (Contributed by NM, 14-Nov-2006.) |
Theorem | zfpair2 3965 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 3964. (Contributed by NM, 14-Nov-2006.) |
Theorem | prexg 3966 | 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 3502, prprc1 3500, and prprc2 3501. (Contributed by Jim Kingdon, 16-Sep-2018.) |
Theorem | snelpwi 3967 | 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 3968 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |
Theorem | prelpwi 3969 | 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 3970* | 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 3971 | 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 3972 | 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 3973 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |
Theorem | pwtr 3974 | 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 3975* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
Theorem | ssext 3976* | 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 3977* | Negation of subclass relationship. Compare nssr 3057. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | pweqb 3978 | 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 3979* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |
Theorem | euabex 3980 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
Theorem | mss 3981* | An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | exss 3982* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
Theorem | opexg 3983 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
Theorem | opex 3984 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | otexg 3985 | An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.) |
Theorem | elop 3986 | 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 3987 | One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opi2 3988 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opm 3989* | An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.) |
Theorem | opnzi 3990 | An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3989). (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth1 3991 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth 3992 | 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 3993 | 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 3994 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth2 3995 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
Theorem | otth2 3996 | Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | otth 3997 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | eqvinop 3998* | A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
Theorem | copsexg 3999* | Substitution of class for ordered pair . (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | copsex2t 4000* | Closed theorem form of copsex2g 4001. (Contributed by NM, 17-Feb-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |