Home | Intuitionistic Logic Explorer Theorem List (p. 41 of 135) | < 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 | opabss 4001* | The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | opabbid 4002 | Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | opabbidv 4003* | Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.) |
Theorem | opabbii 4004 | Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Theorem | nfopab 4005* | Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | nfopab1 4006 | The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | nfopab2 4007 | The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | cbvopab 4008* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.) |
Theorem | cbvopabv 4009* | Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) |
Theorem | cbvopab1 4010* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Theorem | cbvopab2 4011* | Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.) |
Theorem | cbvopab1s 4012* | Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.) |
Theorem | cbvopab1v 4013* | Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
Theorem | cbvopab2v 4014* | Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.) |
Theorem | csbopabg 4015* | Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Theorem | unopab 4016 | Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
Theorem | mpteq12f 4017 | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12dva 4018* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Theorem | mpteq12dv 4019* | An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12 4020* | An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.) |
Theorem | mpteq1 4021* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq1d 4022* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
Theorem | mpteq2ia 4023 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2i 4024 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq12i 4025 | An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2da 4026 | Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpteq2dva 4027* | Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
Theorem | mpteq2dv 4028* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
Theorem | nfmpt 4029* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
Theorem | nfmpt1 4030 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
Theorem | cbvmptf 4031* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Thierry Arnoux, 9-Mar-2017.) |
Theorem | cbvmpt 4032* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.) |
Theorem | cbvmptv 4033* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
Theorem | mptv 4034* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
Syntax | wtr 4035 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
Definition | df-tr 4036 | Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4037 (which is suggestive of the word "transitive"), dftr3 4039, dftr4 4040, and dftr5 4038. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
Theorem | dftr2 4037* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |
Theorem | dftr5 4038* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |
Theorem | dftr3 4039* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
Theorem | dftr4 4040 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
Theorem | treq 4041 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
Theorem | trel 4042 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | trel3 4043 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
Theorem | trss 4044 | An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) |
Theorem | trin 4045 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
Theorem | tr0 4046 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
Theorem | trv 4047 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
Theorem | triun 4048* | The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
Theorem | truni 4049* | The union of a class of transitive sets is transitive. Exercise 5(a) of [Enderton] p. 73. (Contributed by Scott Fenton, 21-Feb-2011.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
Theorem | trint 4050* | The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.) |
Theorem | trintssm 4051* | Any inhabited transitive class includes its intersection. Similar to Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the inhabitedness hypothesis). (Contributed by Jim Kingdon, 22-Aug-2018.) |
Axiom | ax-coll 4052* | Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4105 but uses a freeness hypothesis in place of one of the distinct variable constraints. (Contributed by Jim Kingdon, 23-Aug-2018.) |
Theorem | repizf 4053* | Axiom of Replacement. Axiom 7' of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). In our context this is not an axiom, but a theorem proved from ax-coll 4052. It is identical to zfrep6 4054 except for the choice of a freeness hypothesis rather than a distinct variable constraint between and . (Contributed by Jim Kingdon, 23-Aug-2018.) |
Theorem | zfrep6 4054* | A version of the Axiom of Replacement. Normally would have free variables and . Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4055 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 4055* |
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 2913. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.) |
Theorem | axsep2 4056* | A less restrictive version of the Separation Scheme ax-sep 4055, 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 4055 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Theorem | zfauscl 4057* | Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4055, we invoke the Axiom of Extensionality (indirectly via vtocl 2744), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.) |
Theorem | bm1.3ii 4058* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4055. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |
Theorem | a9evsep 4059* | Derive a weakened version of ax-i9 1511, where and must be distinct, from Separation ax-sep 4055 and Extensionality ax-ext 2122. The theorem also holds (ax9vsep 4060), but in intuitionistic logic is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax9vsep 4060* | Derive a weakened version of ax-9 1512, where and must be distinct, from Separation ax-sep 4055 and Extensionality ax-ext 2122. In intuitionistic logic a9evsep 4059 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | zfnuleu 4061* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2125 to strengthen the hypothesis in the form of axnul 4062). (Contributed by NM, 22-Dec-2007.) |
Theorem | axnul 4062* |
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 4055. 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 4061).
This theorem should not be referenced by any proof. Instead, use ax-nul 4063 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 4063* | The Null Set Axiom of IZF set theory. It was derived as axnul 4062 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 4064 | 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 4063. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | csbexga 4065 | The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Theorem | csbexa 4066 | The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | nalset 4067* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |
Theorem | vnex 4068 | The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.) |
Theorem | vprc 4069 | 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 4070 | The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.) |
Theorem | inex1 4071 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
Theorem | inex2 4072 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |
Theorem | inex1g 4073 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
Theorem | ssex 4074 | 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 4055 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |
Theorem | ssexi 4075 | The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
Theorem | ssexg 4076 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
Theorem | ssexd 4077 | A subclass of a set is a set. Deduction form of ssexg 4076. (Contributed by David Moews, 1-May-2017.) |
Theorem | difexg 4078 | Existence of a difference. (Contributed by NM, 26-May-1998.) |
Theorem | zfausab 4079* | Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) |
Theorem | rabexg 4080* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) |
Theorem | rabex 4081* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.) |
Theorem | elssabg 4082* | Membership in a class abstraction involving a subset. Unlike elabg 2835, does not have to be a set. (Contributed by NM, 29-Aug-2006.) |
Theorem | inteximm 4083* | The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intexr 4084 | If the intersection of a class exists, the class is nonempty. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intnexr 4085 | 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 4086 | The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | intexrabim 4087 | The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | iinexgm 4088* | 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 4089* | 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 4090 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
Theorem | elpw2 4091 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
Theorem | pwnss 4092 | The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Theorem | pwne 4093 | No set equals its power set. The sethood antecedent is necessary; compare pwv 3744. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
Theorem | repizf2lem 4094 | Lemma for repizf2 4095. 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 4095* | Replacement. This version of replacement is stronger than repizf 4053 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 4053 with ax-sep 4055. Another variation would be but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.) |
Theorem | class2seteq 4096* | Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |
Theorem | 0elpw 4097 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
Theorem | 0nep0 4098 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |
Theorem | 0inp0 4099 | 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 4100 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |