Home | Metamath
Proof ExplorerTheorem List
(p. 42 of 314)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21444) |
Hilbert Space Explorer
(21445-22967) |
Users' Mathboxes
(22968-31305) |

Type | Label | Description |
---|---|---|

Statement | ||

Axiom | ax-sep 4101* | The Axiom of Separation of ZF set theory. See axsep 4100 for more information. It was derived as axsep 4100 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 11-Sep-2006.) |

Theorem | axsep2 4102* | A less restrictive version of the Separation Scheme axsep 4100, 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 4101 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |

Theorem | zfauscl 4103* |
Separation Scheme (Aussonderung) using a class variable. To derive this
from ax-sep 4101, we invoke the Axiom of Extensionality
(indirectly via
vtocl 2806), which is needed for the justification of
class variable
notation.
If we omit the requirement that not occur in , we can derive a contradiction, as notzfaus 4143 shows. (Contributed by NM, 5-Aug-1993.) |

Theorem | bm1.3ii 4104* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4101. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |

Theorem | ax9vsep 4105* | Derive a weakened version of ax-9 1684 ( i.e. ax-9v 1632), where and must be distinct, from Separation ax-sep 4101 and Extensionality ax-ext 2237. See ax9 1683 for the derivation of ax-9 1684 from ax-9v 1632. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |

2.2.3 Derive the Null Set Axiom | ||

Theorem | zfnuleu 4106* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2241 to strengthen the hypothesis in the form of axnul 4108). (Contributed by NM, 22-Dec-2007.) |

Theorem | axnulALT 4107* | Prove axnul 4108 directly from ax-rep 4091 without using any equality axioms (ax-9 1684 thru ax-16 1927) if we accept ax-4 1692 as an axiom. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (Proof modification is discouraged.) |

Theorem | axnul 4108* |
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 4101. This version of the Null Set Axiom tells us
that at least one empty set exists, but does not tells us that it is
unique - we need the Axiom of Extensionality to do that (see
zfnuleu 4106).
This proof, suggested by Jeff Hoffman (3-Feb-2008), uses only ax-5 1533 and ax-gen 1536 from predicate calculus, which are valid in "free logic" i.e. logic holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc] p. 277). Thus our ax-sep 4101 implies the existence of at least one set. Note that Kunen's version of ax-sep 4101 (Axiom 3 of [Kunen] p. 11) does not imply the existence of a set because his is universally closed i.e. prefixed with universal quantifiers to eliminate all free variables. His existence is provided by a separate axiom stating (Axiom 0 of [Kunen] p. 10). See axnulALT 4107 for a proof directly from ax-rep 4091. This theorem should not be referenced by any proof. Instead, use ax-nul 4109 below so that the uses of the Null Set Axiom can be more easily identified. (Contributed by NM, 7-Aug-2003.) (Revised by NM, 4-Feb-2008.) (New usage is discouraged.) |

Axiom | ax-nul 4109* | The Null Set Axiom of ZF set theory. It was derived as axnul 4108 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 7-Aug-2003.) |

Theorem | 0ex 4110 | 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 4109. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |

2.2.4 Theorems requiring subset and intersection
existence | ||

Theorem | nalset 4111* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |

Theorem | vprc 4112 | 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 4113 | The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.) |

Theorem | vnex 4114 | The universal class does not exist. (Contributed by NM, 4-Jul-2005.) |

Theorem | inex1 4115 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |

Theorem | inex2 4116 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |

Theorem | inex1g 4117 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |

Theorem | ssex 4118 | 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 4101 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |

Theorem | ssexi 4119 | The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |

Theorem | ssexg 4120 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |

Theorem | ssexd 4121 | A subclass of a set is a set. Deduction form of ssexg 4120. (Contributed by David Moews, 1-May-2017.) |

Theorem | difexg 4122 | Existence of a difference. (Contributed by NM, 26-May-1998.) |

Theorem | zfausab 4123* | Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) |

Theorem | rabexg 4124* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) |

Theorem | rabex 4125* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.) |

Theorem | elssabg 4126* | Membership in a class abstraction involving a subset. Unlike elabg 2883, does not have to be a set. (Contributed by NM, 29-Aug-2006.) |

Theorem | elpw2g 4127 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |

Theorem | elpw2 4128 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |

Theorem | intex 4129 | The intersection of a non-empty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.) |

Theorem | intnex 4130 | If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005.) |

Theorem | intexab 4131 | The intersection of a non-empty class abstraction exists. (Contributed by NM, 21-Oct-2003.) |

Theorem | intexrab 4132 | The intersection of a non-empty restricted class abstraction exists. (Contributed by NM, 21-Oct-2003.) |

Theorem | iinexg 4133* | The existence of an indexed union. is normally a free-variable parameter in , which should be read . (Contributed by FL, 19-Sep-2011.) |

Theorem | intabs 4134* | Absorption of a redundant conjunct in the intersection of a class abstraction. (Contributed by NM, 3-Jul-2005.) |

Theorem | inuni 4135* | 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.) |

2.2.5 Theorems requiring empty set
existence | ||

Theorem | class2set 4136* | Construct, from any class , a set equal to it when the class exists and equal to the empty set when the class is proper. This theorem shows that the constructed set always exists. (Contributed by NM, 16-Oct-2003.) |

Theorem | class2seteq 4137* | Equality theorem based on class2set 4136. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |

Theorem | 0elpw 4138 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |

Theorem | 0nep0 4139 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |

Theorem | 0inp0 4140 | 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 4141 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |

Theorem | iin0 4142* | An indexed intersection of the empty set, with a non-empty index set, is empty. (Contributed by NM, 20-Oct-2005.) |

Theorem | notzfaus 4143* | In the Separation Scheme zfauscl 4103, we require that not occur in (which can be generalized to "not be free in"). Here we show special cases of and that result in a contradiction by violating this requirement. (Contributed by NM, 8-Feb-2006.) |

Theorem | intv 4144 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |

Theorem | axpweq 4145* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 4146 is not used by the proof. (Contributed by NM, 22-Jun-2009.) |

2.3 ZF Set Theory - add the Axiom of Power
Sets | ||

2.3.1 Introduce the Axiom of Power
Sets | ||

Axiom | ax-pow 4146* | Axiom of Power Sets. An axiom of 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 . The variant axpow2 4148 uses explicit subset notation. A version using class notation is pwex 4151. (Contributed by NM, 5-Aug-1993.) |

Theorem | zfpow 4147* | Axiom of Power Sets expressed with fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |

Theorem | axpow2 4148* | A variant of the Axiom of Power Sets ax-pow 4146 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |

Theorem | axpow3 4149* | A variant of the Axiom of Power Sets ax-pow 4146. 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 4150* | Every set is an element of some other set. See elALT 4176 for a shorter proof using more axioms. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |

Theorem | pwex 4151 | 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 4152 | 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 4153* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |

Theorem | snexALT 4154 | A singleton is a set. Theorem 7.13 of [Quine] p. 51, but proved using only Extensionality, Power Set, and Separation. Unlike the proof of zfpair 4170, Replacement is not needed. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) See also snex 4174. (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | p0ex 4155 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |

Theorem | p0exALT 4156 | The power set of the empty set (the ordinal 1) is a set. Alternate proof. (Contributed by NM, 23-Dec-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | pp0ex 4157 | The power set of the power set of the empty set (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |

Theorem | ord3ex 4158 | The ordinal number 3 is a set, proved without the Axiom of Union ax-un 4470. (Contributed by NM, 2-May-2009.) |

Theorem | dtru 4159* |
At least two sets exist (or in terms of first-order logic, the universe
of discourse has two or more objects). Note that we may not substitute
the same variable for both and (as
indicated by the distinct
variable requirement), for otherwise we would contradict stdpc6 1821.
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2237 or ax-sep 4101. See dtruALT 4165 for a shorter proof using these axioms. The proof makes use of dummy variables and which do not appear in the final theorem. They must be distinct from each other and from and . In other words, if we were to substitute for throughout the proof, the proof would fail. Although this requirement is made explicitly in the set.mm source file, it is implicit on the web page (i.e. doesn't appear in the "Distinct variable group"). (Contributed by NM, 7-Nov-2006.) |

Theorem | ax16b 4160* | This theorem shows that axiom ax-16 1927 is redundant in the presence of theorem dtru 4159, which states simply that at least two things exist. This justifies the remark at http://us.metamath.org/mpegif/mmzfcnd.html#twoness (which links to this theorem). (Contributed by NM, 7-Nov-2006.) |

Theorem | eunex 4161 | Existential uniqueness implies there is a value for which the wff argument is false. (Contributed by NM, 24-Oct-2010.) |

Theorem | nfnid 4162 | A set variable is not free from itself. The proof relies on dtru 4159, that is, it is not true in a one-element domain. (Contributed by Mario Carneiro, 8-Oct-2016.) |

Theorem | nfcvb 4163* | The "distinctor" expression , stating that and are not the same variable, can be written in terms of in the obvious way. This theorem is not true in a one-element domain, because then and will both be true. (Contributed by Mario Carneiro, 8-Oct-2016.) |

Theorem | pwuni 4164 | 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.) |

Theorem | dtruALT 4165* |
A version of dtru 4159 ("two things exist") with a shorter
proof that uses
more axioms but may be easier to understand.
Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that and be distinct. Specifically, theorem cla4ev 2843 requires that must not occur in the subexpression in step 4 nor in the subexpression in step 9. The proof verifier will require that and be in a distinct variable group to ensure this. You can check this by deleting the $d statement in set.mm and rerunning the verifier, which will print a detailed explanation of the distinct variable violation. (Contributed by NM, 15-Jul-1994.) (Proof modification is discouraged.) |

Theorem | dtrucor 4166* | Corollary of dtru 4159. This example illustrates the danger of blindly trusting the standard Deduction Theorem without accounting for free variables: the theorem form of this deduction is not valid, as shown by dtrucor2 4167. (Contributed by NM, 27-Jun-2002.) |

Theorem | dtrucor2 4167 | The theorem form of the deduction dtrucor 4166 leads to a contradiction, as mentioned in the "Wrong!" example at http://us.metamath.org/mpegif/mmdeduction.html#bad. (Contributed by NM, 20-Oct-2007.) |

Theorem | dvdemo1 4168* | Demonstration of a theorem (scheme) that requires (meta)variables and to be distinct, but no others. It bundles the theorem schemes and . Compare dvdemo2 4169. ("Bundles" is a term introduced by Raph Levien.) (Contributed by NM, 1-Dec-2006.) |

Theorem | dvdemo2 4169* | Demonstration of a theorem (scheme) that requires (meta)variables and to be distinct, but no others. It bundles the theorem schemes and . Compare dvdemo1 4168. (Contributed by NM, 1-Dec-2006.) |

2.3.2 Derive the Axiom of Pairing | ||

Theorem | zfpair 4170 |
The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of
[TakeutiZaring] p. 15. In some
textbooks this is stated as a separate
axiom; here we show it is redundant since it can be derived from the
other axioms.
This theorem should not be referenced by any proof other than axpr 4171. Instead, use zfpair2 4173 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |

Theorem | axpr 4171* |
Unabbreviated version of the Axiom of Pairing of ZF set theory, derived
as a theorem from the other axioms.
This theorem should not be referenced by any proof. Instead, use ax-pr 4172 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.) |

Axiom | ax-pr 4172* | The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 4171 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 14-Nov-2006.) |

Theorem | zfpair2 4173 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 4172. See zfpair 4170 for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006.) |

Theorem | snex 4174 | A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4154. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.) |

Theorem | prex 4175 | The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc 3698), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 5-Aug-1993.) |

Theorem | elALT 4176* | Every set is an element of some other set. This has a shorter proof than el 4150 but uses more axioms. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) |

Theorem | dtruALT2 4177* | An alternative proof of dtru 4159 ("two things exist") using ax-pr 4172 instead of ax-pow 4146. (Contributed by Mario Carneiro, 31-Aug-2015.) (Proof modification is discouraged.) |

Theorem | snelpwi 4178 | 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 4179 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |

Theorem | rext 4180* | 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 4181 | 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 4182 | 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 4183 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |

Theorem | pwtr 4184 | 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 4185* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |

Theorem | ssext 4186* | 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 | nssss 4187* | Negation of subclass relationship. Compare nss 3197. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |

Theorem | pweqb 4188 | 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 4189* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |

Theorem | moabex 4190 | "At most one" existence implies a class abstraction exists. (Contributed by NM, 30-Dec-1996.) |

Theorem | rmorabex 4191 | Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.) |

Theorem | euabex 4192 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |

Theorem | nnullss 4193* | A non-empty class (even if proper) has a non-empty subset. (Contributed by NM, 23-Aug-2003.) |

Theorem | exss 4194* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |

Theorem | opex 4195 | An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |

Theorem | otex 4196 | An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015.) |

Theorem | elop 4197 | 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 4198 | One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |

Theorem | opi2 4199 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |

2.3.3 Ordered pair theorem | ||

Theorem | opnz 4200 | An ordered pair is nonempty iff the arguments are sets. (Contributed by NM, 24-Jan-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |