Home | Intuitionistic Logic Explorer Theorem List (p. 40 of 105) | < 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 | zfrep6 3901* | A version of the Axiom of Replacement. Normally would have free variables and . Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 3902 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version. (Contributed by NM, 10-Oct-2003.) |
Axiom | ax-sep 3902* |
The Axiom of Separation of IZF set theory. Axiom 6 of [Crosilla], p.
"Axioms of CZF and IZF" (with unnecessary quantifier removed,
and with a
condition replaced by a distinct
variable constraint between
and ).
The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with ) so that it asserts the existence of a collection only if it is smaller than some other collection that already exists. This prevents Russell's paradox ru 2785. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.) |
Theorem | axsep2 3903* | A less restrictive version of the Separation Scheme ax-sep 3902, where variables and can both appear free in the wff , which can therefore be thought of as . This version was derived from the more restrictive ax-sep 3902 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Theorem | zfauscl 3904* | Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 3902, we invoke the Axiom of Extensionality (indirectly via vtocl 2625), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.) |
Theorem | bm1.3ii 3905* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 3902. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |
Theorem | a9evsep 3906* | Derive a weakened version of ax-i9 1439, where and must be distinct, from Separation ax-sep 3902 and Extensionality ax-ext 2038. The theorem also holds (ax9vsep 3907), but in intuitionistic logic is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax9vsep 3907* | Derive a weakened version of ax-9 1440, where and must be distinct, from Separation ax-sep 3902 and Extensionality ax-ext 2038. In intuitionistic logic a9evsep 3906 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | zfnuleu 3908* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2041 to strengthen the hypothesis in the form of axnul 3909). (Contributed by NM, 22-Dec-2007.) |
Theorem | axnul 3909* |
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 3902. 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 3908).
This theorem should not be referenced by any proof. Instead, use ax-nul 3910 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 3910* | The Null Set Axiom of IZF set theory. It was derived as axnul 3909 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 3911 | 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 3910. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | csbexga 3912 | The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Theorem | csbexa 3913 | The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | nalset 3914* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |
Theorem | vprc 3915 | 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 3916 | The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.) |
Theorem | vnex 3917 | The universal class does not exist. (Contributed by NM, 4-Jul-2005.) |
Theorem | inex1 3918 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
Theorem | inex2 3919 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |
Theorem | inex1g 3920 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
Theorem | ssex 3921 | 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 3902 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |
Theorem | ssexi 3922 | The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
Theorem | ssexg 3923 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
Theorem | ssexd 3924 | A subclass of a set is a set. Deduction form of ssexg 3923. (Contributed by David Moews, 1-May-2017.) |
Theorem | difexg 3925 | Existence of a difference. (Contributed by NM, 26-May-1998.) |
Theorem | zfausab 3926* | Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) |
Theorem | rabexg 3927* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) |
Theorem | rabex 3928* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.) |
Theorem | elssabg 3929* | Membership in a class abstraction involving a subset. Unlike elabg 2710, does not have to be a set. (Contributed by NM, 29-Aug-2006.) |
Theorem | inteximm 3930* | The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intexr 3931 | If the intersection of a class exists, the class is non-empty. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intnexr 3932 | 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 3933 | The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intexrabim 3934 | The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | iinexgm 3935* | 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 3936* | 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 3937 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
Theorem | elpw2 3938 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
Theorem | pwnss 3939 | The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Theorem | pwne 3940 | No set equals its power set. The sethood antecedent is necessary; compare pwv 3606. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
Theorem | repizf2lem 3941 | Lemma for repizf2 3942. 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 3942* | Replacement. This version of replacement is stronger than repizf 3900 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 3900 with ax-sep 3902. Another variation would be but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.) |
Theorem | class2seteq 3943* | Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |
Theorem | 0elpw 3944 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
Theorem | 0nep0 3945 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |
Theorem | 0inp0 3946 | 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 3947 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |
Theorem | iin0imm 3948* | An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
Theorem | iin0r 3949* | 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 3950 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |
Theorem | axpweq 3951* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 3954 is not used by the proof. (Contributed by NM, 22-Jun-2009.) |
Theorem | bnd 3952* | A very strong generalization of the Axiom of Replacement (compare zfrep6 3901). 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 3899. (Contributed by NM, 17-Oct-2004.) |
Theorem | bnd2 3953* | A variant of the Boundedness Axiom bnd 3952 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 3954* |
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 3905).
The variant axpow2 3956 uses explicit subset notation. A version using class notation is pwex 3959. (Contributed by NM, 5-Aug-1993.) |
Theorem | zfpow 3955* | Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
Theorem | axpow2 3956* | A variant of the Axiom of Power Sets ax-pow 3954 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
Theorem | axpow3 3957* | A variant of the Axiom of Power Sets ax-pow 3954. 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 3958* | 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 3959 | 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 3960 | 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 3961* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | snexgOLD 3962 | 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 3963 and new proofs should use snexg 3963 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of snexg 3963 and then remove it. |
Theorem | snexg 3963 | 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 3964 | A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | snexprc 3965 | 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 3966 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |
Theorem | pp0ex 3967 | (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |
Theorem | ord3ex 3968 | The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.) |
Theorem | dtruarb 3969* | 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 4310 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 3970 | 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 3971* | 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 3905). (Contributed by NM, 14-Nov-2006.) |
Theorem | zfpair2 3972 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 3971. (Contributed by NM, 14-Nov-2006.) |
Theorem | prexgOLD 3973 | 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 3507, prprc1 3505, and prprc2 3506. This is a special case of prexg 3974 and new proofs should use prexg 3974 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of prexg 3974 and then remove it. |
Theorem | prexg 3974 | 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 3507, prprc1 3505, and prprc2 3506. (Contributed by Jim Kingdon, 16-Sep-2018.) |
Theorem | snelpwi 3975 | 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 3976 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |
Theorem | prelpwi 3977 | 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 3978* | 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 3979 | 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 3980 | 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 3981 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |
Theorem | pwtr 3982 | 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 3983* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
Theorem | ssext 3984* | 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 3985* | Negation of subclass relationship. Compare nssr 3030. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | pweqb 3986 | 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 3987* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |
Theorem | euabex 3988 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
Theorem | mss 3989* | An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | exss 3990* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
Theorem | opexg 3991 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
Theorem | opexgOLD 3992 | An ordered pair of sets is a set. This is a special case of opexg 3991 and new proofs should use opexg 3991 instead. (Contributed by Jim Kingdon, 19-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of opexg 3991 and then remove it. |
Theorem | opex 3993 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | otexg 3994 | An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.) |
Theorem | elop 3995 | 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 3996 | One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opi2 3997 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opm 3998* | An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.) |
Theorem | opnzi 3999 | An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3998). (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth1 4000 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |