Home | Intuitionistic Logic Explorer Theorem List (p. 40 of 102) | < 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 | rabex 3901* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.) |
Theorem | elssabg 3902* | Membership in a class abstraction involving a subset. Unlike elabg 2688, does not have to be a set. (Contributed by NM, 29-Aug-2006.) |
Theorem | inteximm 3903* | The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intexr 3904 | If the intersection of a class exists, the class is non-empty. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intnexr 3905 | 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 3906 | The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intexrabim 3907 | The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | iinexgm 3908* | 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 3909* | 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 3910 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
Theorem | elpw2 3911 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
Theorem | pwnss 3912 | The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Theorem | pwne 3913 | No set equals its power set. The sethood antecedent is necessary; compare pwv 3579. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
Theorem | repizf2lem 3914 | Lemma for repizf2 3915. 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 3915* | Replacement. This version of replacement is stronger than repizf 3873 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 3873 with ax-sep 3875. Another variation would be but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.) |
Theorem | class2seteq 3916* | Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |
Theorem | 0elpw 3917 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
Theorem | 0nep0 3918 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |
Theorem | 0inp0 3919 | 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 3920 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |
Theorem | iin0imm 3921* | An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
Theorem | iin0r 3922* | 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 3923 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |
Theorem | axpweq 3924* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 3927 is not used by the proof. (Contributed by NM, 22-Jun-2009.) |
Theorem | bnd 3925* | A very strong generalization of the Axiom of Replacement (compare zfrep6 3874). 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 3872. (Contributed by NM, 17-Oct-2004.) |
Theorem | bnd2 3926* | A variant of the Boundedness Axiom bnd 3925 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 3927* |
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 3878).
The variant axpow2 3929 uses explicit subset notation. A version using class notation is pwex 3932. (Contributed by NM, 5-Aug-1993.) |
Theorem | zfpow 3928* | Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
Theorem | axpow2 3929* | A variant of the Axiom of Power Sets ax-pow 3927 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
Theorem | axpow3 3930* | A variant of the Axiom of Power Sets ax-pow 3927. 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 3931* | 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 3932 | 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 3933 | 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 3934* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | snexgOLD 3935 | 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 3936 and new proofs should use snexg 3936 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of snexg 3936 and then remove it. |
Theorem | snexg 3936 | 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 3937 | A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | snexprc 3938 | 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 3939 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |
Theorem | pp0ex 3940 | (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |
Theorem | ord3ex 3941 | The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.) |
Theorem | dtruarb 3942* | 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 4283 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 3943 | 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 3944* | 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 3878). (Contributed by NM, 14-Nov-2006.) |
Theorem | zfpair2 3945 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 3944. (Contributed by NM, 14-Nov-2006.) |
Theorem | prexgOLD 3946 | 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 3480, prprc1 3478, and prprc2 3479. This is a special case of prexg 3947 and new proofs should use prexg 3947 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of prexg 3947 and then remove it. |
Theorem | prexg 3947 | 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 3480, prprc1 3478, and prprc2 3479. (Contributed by Jim Kingdon, 16-Sep-2018.) |
Theorem | snelpwi 3948 | 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 3949 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |
Theorem | prelpwi 3950 | 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 3951* | 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 3952 | 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 3953 | 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 3954 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |
Theorem | pwtr 3955 | 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 3956* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
Theorem | ssext 3957* | 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 3958* | Negation of subclass relationship. Compare nssr 3003. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | pweqb 3959 | 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 3960* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |
Theorem | euabex 3961 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
Theorem | mss 3962* | An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.) |
Theorem | exss 3963* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
Theorem | opexg 3964 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
Theorem | opexgOLD 3965 | An ordered pair of sets is a set. This is a special case of opexg 3964 and new proofs should use opexg 3964 instead. (Contributed by Jim Kingdon, 19-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of opexg 3964 and then remove it. |
Theorem | opex 3966 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | otexg 3967 | An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.) |
Theorem | elop 3968 | 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 3969 | One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opi2 3970 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opm 3971* | An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.) |
Theorem | opnzi 3972 | An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3971). (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth1 3973 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth 3974 | 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 3975 | 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 3976 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth2 3977 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
Theorem | otth2 3978 | Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | otth 3979 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | eqvinop 3980* | A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
Theorem | copsexg 3981* | Substitution of class for ordered pair . (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | copsex2t 3982* | Closed theorem form of copsex2g 3983. (Contributed by NM, 17-Feb-2013.) |
Theorem | copsex2g 3983* | Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) |
Theorem | copsex4g 3984* | An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.) |
Theorem | 0nelop 3985 | A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opeqex 3986 | Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.) |
Theorem | opcom 3987 | An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.) |
Theorem | moop2 3988* | "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opeqsn 3989 | Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) |
Theorem | opeqpr 3990 | Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) |
Theorem | euotd 3991* | Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.) |
Theorem | uniop 3992 | 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 3993 | Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opabid 3994 | 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 3995* | Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.) |
Theorem | opelopabsbALT 3996* | The law of concretion in terms of substitutions. Less general than opelopabsb 3997, 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 3997* | The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
Theorem | brabsb 3998* | The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.) |
Theorem | opelopabt 3999* | Closed theorem form of opelopab 4008. (Contributed by NM, 19-Feb-2013.) |
Theorem | opelopabga 4000* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |