![]() |
Intuitionistic Logic Explorer Theorem List (p. 42 of 154) | < 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 | mpteq12 4101* | An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mpteq1 4102* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mpteq1d 4103* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mpteq2ia 4104 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mpteq2i 4105 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mpteq12i 4106 | An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mpteq2da 4107 | 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 4108* | Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mpteq2dv 4109* | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nfmpt 4110* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nfmpt1 4111 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cbvmptf 4112* | 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 4113* | 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 4114* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | mptv 4115* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wtr 4116 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |
![]() ![]() ![]() | ||
Definition | df-tr 4117 | Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4118 (which is suggestive of the word "transitive"), dftr3 4120, dftr4 4121, and dftr5 4119. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dftr2 4118* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dftr5 4119* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dftr3 4120* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | dftr4 4121 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | treq 4122 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | trel 4123 | 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 4124 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | trss 4125 | An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | trin 4126 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | tr0 4127 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |
![]() ![]() ![]() | ||
Theorem | trv 4128 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |
![]() ![]() ![]() | ||
Theorem | triun 4129* | The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | truni 4130* | 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 4131* | 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 4132* | 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 4133* | Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4190 but uses a freeness hypothesis in place of one of the distinct variable conditions. (Contributed by Jim Kingdon, 23-Aug-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | repizf 4134* |
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 4133. It is identical to
zfrep6 4135 except for the choice of a freeness
hypothesis rather than a
disjoint variable condition between ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | zfrep6 4135* |
A version of the Axiom of Replacement. Normally ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-sep 4136* |
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
![]() ![]() ![]() ![]() ![]()
The Separation Scheme is a weak form of Frege's Axiom of Comprehension,
conditioning it (with (Contributed by NM, 11-Sep-2006.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axsep2 4137* |
A less restrictive version of the Separation Scheme ax-sep 4136, where
variables ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | zfauscl 4138* | Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4136, we invoke the Axiom of Extensionality (indirectly via vtocl 2806), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bm1.3ii 4139* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4136. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | a9evsep 4140* |
Derive a weakened version of ax-i9 1541, where ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax9vsep 4141* |
Derive a weakened version of ax-9 1542, where ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | zfnuleu 4142* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2174 to strengthen the hypothesis in the form of axnul 4143). (Contributed by NM, 22-Dec-2007.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axnul 4143* |
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 4136. 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 4142).
This theorem should not be referenced by any proof. Instead, use ax-nul 4144 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 4144* | The Null Set Axiom of IZF set theory. It was derived as axnul 4143 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 4145 | 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 4144. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
![]() ![]() ![]() ![]() | ||
Theorem | csbexga 4146 | The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | csbexa 4147 | The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nalset 4148* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | vnex 4149 | The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | vprc 4150 | 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 4151 | The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | inex1 4152 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | inex2 4153 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | inex1g 4154 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ssex 4155 | 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 4136 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ssexi 4156 | The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ssexg 4157 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ssexd 4158 | A subclass of a set is a set. Deduction form of ssexg 4157. (Contributed by David Moews, 1-May-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | difexg 4159 | Existence of a difference. (Contributed by NM, 26-May-1998.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | zfausab 4160* | Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | rabexg 4161* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | rabex 4162* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | rabexd 4163* | Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 4164. (Contributed by AV, 16-Jul-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | rabex2 4164* | Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | rab2ex 4165* | A class abstraction based on a class abstraction based on a set is a set. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elssabg 4166* |
Membership in a class abstraction involving a subset. Unlike elabg 2898,
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | inteximm 4167* | The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | intexr 4168 | If the intersection of a class exists, the class is nonempty. (Contributed by Jim Kingdon, 27-Aug-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | intnexr 4169 | 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 4170 | The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | intexrabim 4171 | The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | iinexgm 4172* |
The existence of an indexed union. ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | inuni 4173* |
The intersection of a union ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elpw2g 4174 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elpw2 4175 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elpwi2 4176 | Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | pwnss 4177 | The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | pwne 4178 | No set equals its power set. The sethood antecedent is necessary; compare pwv 3823. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | repizf2lem 4179 |
Lemma for repizf2 4180. If we have a function-like proposition
which
provides at most one value of ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | repizf2 4180* |
Replacement. This version of replacement is stronger than repizf 4134 in
the sense that ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | class2seteq 4181* | Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0elpw 4182 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0nep0 4183 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0inp0 4184 | 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 4185 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | iin0imm 4186* | An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | iin0r 4187* | If an indexed intersection of the empty set is empty, the index set is nonempty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | intv 4188 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | axpweq 4189* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 4192 is not used by the proof. (Contributed by NM, 22-Jun-2009.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bnd 4190* |
A very strong generalization of the Axiom of Replacement (compare
zfrep6 4135). Its strength lies in the rather profound
fact that
![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | bnd2 4191* |
A variant of the Boundedness Axiom bnd 4190 that picks a subset ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-pow 4192* |
Axiom of Power Sets. An axiom of Intuitionistic Zermelo-Fraenkel set
theory. It states that a set ![]() ![]() ![]() The variant axpow2 4194 uses explicit subset notation. A version using class notation is pwex 4201. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | zfpow 4193* | Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axpow2 4194* | A variant of the Axiom of Power Sets ax-pow 4192 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | axpow3 4195* |
A variant of the Axiom of Power Sets ax-pow 4192. For any set ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | el 4196* | Every set is an element of some other set. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | vpwex 4197 | Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 4198 from vpwex 4197. (Revised by BJ, 10-Aug-2022.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | pwexg 4198 | Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | pwexd 4199 | Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | abssexg 4200* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |