Home Intuitionistic Logic ExplorerTheorem List (p. 40 of 106) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 3901-4000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremrepizf 3901* 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 3900. It is identical to zfrep6 3902 except for the choice of a freeness hypothesis rather than a distinct variable constraint between 𝑏 and 𝜑. (Contributed by Jim Kingdon, 23-Aug-2018.)
𝑏𝜑       (∀𝑥𝑎 ∃!𝑦𝜑 → ∃𝑏𝑥𝑎𝑦𝑏 𝜑)

Theoremzfrep6 3902* A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 3903 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.)
(∀𝑥𝑧 ∃!𝑦𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑)

2.2.2  Introduce the Axiom of Separation

Axiomax-sep 3903* 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 2786. In some texts, this scheme is called "Aussonderung" or the Subset Axiom.

(Contributed by NM, 11-Sep-2006.)

𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))

Theoremaxsep2 3904* A less restrictive version of the Separation Scheme ax-sep 3903, 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 3903 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))

Theoremzfauscl 3905* Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 3903, 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.)
𝐴 ∈ V       𝑦𝑥(𝑥𝑦 ↔ (𝑥𝐴𝜑))

Theorembm1.3ii 3906* Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 3903. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.)
𝑥𝑦(𝜑𝑦𝑥)       𝑥𝑦(𝑦𝑥𝜑)

Theorema9evsep 3907* Derive a weakened version of ax-i9 1439, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 3903 and Extensionality ax-ext 2038. The theorem ¬ ∀𝑥¬ 𝑥 = 𝑦 also holds (ax9vsep 3908), but in intuitionistic logic 𝑥𝑥 = 𝑦 is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
𝑥 𝑥 = 𝑦

Theoremax9vsep 3908* Derive a weakened version of ax-9 1440, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 3903 and Extensionality ax-ext 2038. In intuitionistic logic a9evsep 3907 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
¬ ∀𝑥 ¬ 𝑥 = 𝑦

2.2.3  Derive the Null Set Axiom

Theoremzfnuleu 3909* 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 3910). (Contributed by NM, 22-Dec-2007.)
𝑥𝑦 ¬ 𝑦𝑥       ∃!𝑥𝑦 ¬ 𝑦𝑥

Theoremaxnul 3910* 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 3903. 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 3909).

This theorem should not be referenced by any proof. Instead, use ax-nul 3911 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.)

𝑥𝑦 ¬ 𝑦𝑥

Axiomax-nul 3911* The Null Set Axiom of IZF set theory. It was derived as axnul 3910 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.)
𝑥𝑦 ¬ 𝑦𝑥

Theorem0ex 3912 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 3911. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
∅ ∈ V

Theoremcsbexga 3913 The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
((𝐴𝑉 ∧ ∀𝑥 𝐵𝑊) → 𝐴 / 𝑥𝐵 ∈ V)

Theoremcsbexa 3914 The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
𝐴 ∈ V    &   𝐵 ∈ V       𝐴 / 𝑥𝐵 ∈ V

2.2.4  Theorems requiring subset and intersection existence

Theoremnalset 3915* No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.)
¬ ∃𝑥𝑦 𝑦𝑥

Theoremvprc 3916 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.)
¬ V ∈ V

Theoremnvel 3917 The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.)
¬ V ∈ 𝐴

Theoremvnex 3918 The universal class does not exist. (Contributed by NM, 4-Jul-2005.)
¬ ∃𝑥 𝑥 = V

Theoreminex1 3919 Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
𝐴 ∈ V       (𝐴𝐵) ∈ V

Theoreminex2 3920 Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
𝐴 ∈ V       (𝐵𝐴) ∈ V

Theoreminex1g 3921 Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
(𝐴𝑉 → (𝐴𝐵) ∈ V)

Theoremssex 3922 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 3903 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
𝐵 ∈ V       (𝐴𝐵𝐴 ∈ V)

Theoremssexi 3923 The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
𝐵 ∈ V    &   𝐴𝐵       𝐴 ∈ V

Theoremssexg 3924 The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)
((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)

Theoremssexd 3925 A subclass of a set is a set. Deduction form of ssexg 3924. (Contributed by David Moews, 1-May-2017.)
(𝜑𝐵𝐶)    &   (𝜑𝐴𝐵)       (𝜑𝐴 ∈ V)

Theoremdifexg 3926 Existence of a difference. (Contributed by NM, 26-May-1998.)
(𝐴𝑉 → (𝐴𝐵) ∈ V)

Theoremzfausab 3927* Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.)
𝐴 ∈ V       {𝑥 ∣ (𝑥𝐴𝜑)} ∈ V

Theoremrabexg 3928* Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)
(𝐴𝑉 → {𝑥𝐴𝜑} ∈ V)

Theoremrabex 3929* Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
𝐴 ∈ V       {𝑥𝐴𝜑} ∈ V

Theoremelssabg 3930* Membership in a class abstraction involving a subset. Unlike elabg 2711, 𝐴 does not have to be a set. (Contributed by NM, 29-Aug-2006.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐵𝑉 → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))

Theoreminteximm 3931* The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
(∃𝑥 𝑥𝐴 𝐴 ∈ V)

Theoremintexr 3932 If the intersection of a class exists, the class is non-empty. (Contributed by Jim Kingdon, 27-Aug-2018.)
( 𝐴 ∈ V → 𝐴 ≠ ∅)

Theoremintnexr 3933 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.)
( 𝐴 = V → ¬ 𝐴 ∈ V)

Theoremintexabim 3934 The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
(∃𝑥𝜑 {𝑥𝜑} ∈ V)

Theoremintexrabim 3935 The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.)
(∃𝑥𝐴 𝜑 {𝑥𝐴𝜑} ∈ V)

Theoremiinexgm 3936* The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵, which should be read 𝐵(𝑥). (Contributed by Jim Kingdon, 28-Aug-2018.)
((∃𝑥 𝑥𝐴 ∧ ∀𝑥𝐴 𝐵𝐶) → 𝑥𝐴 𝐵 ∈ V)

Theoreminuni 3937* 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.)
( 𝐴𝐵) = {𝑥 ∣ ∃𝑦𝐴 𝑥 = (𝑦𝐵)}

Theoremelpw2g 3938 Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
(𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))

Theoremelpw2 3939 Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
𝐵 ∈ V       (𝐴 ∈ 𝒫 𝐵𝐴𝐵)

Theorempwnss 3940 The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.)
(𝐴𝑉 → ¬ 𝒫 𝐴𝐴)

Theorempwne 3941 No set equals its power set. The sethood antecedent is necessary; compare pwv 3607. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
(𝐴𝑉 → 𝒫 𝐴𝐴)

Theoremrepizf2lem 3942 Lemma for repizf2 3943. 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.)
(∀𝑥𝑤 ∃*𝑦𝜑 ↔ ∀𝑥 ∈ {𝑥𝑤 ∣ ∃𝑦𝜑}∃!𝑦𝜑)

Theoremrepizf2 3943* Replacement. This version of replacement is stronger than repizf 3901 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 3901 with ax-sep 3903. Another variation would be 𝑥𝑤∃*𝑦𝜑 → {𝑦 ∣ ∃𝑥(𝑥𝑤𝜑)} ∈ V but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.)
𝑧𝜑       (∀𝑥𝑤 ∃*𝑦𝜑 → ∃𝑧𝑥 ∈ {𝑥𝑤 ∣ ∃𝑦𝜑}∃𝑦𝑧 𝜑)

2.2.5  Theorems requiring empty set existence

Theoremclass2seteq 3944* Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.)
(𝐴𝑉 → {𝑥𝐴𝐴 ∈ V} = 𝐴)

Theorem0elpw 3945 Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
∅ ∈ 𝒫 𝐴

Theorem0nep0 3946 The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)
∅ ≠ {∅}

Theorem0inp0 3947 Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 30-Sep-2003.)
(𝐴 = ∅ → ¬ 𝐴 = {∅})

Theoremunidif0 3948 The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.)
(𝐴 ∖ {∅}) = 𝐴

Theoremiin0imm 3949* An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.)
(∃𝑦 𝑦𝐴 𝑥𝐴 ∅ = ∅)

Theoremiin0r 3950* If an indexed intersection of the empty set is empty, the index set is non-empty. (Contributed by Jim Kingdon, 29-Aug-2018.)
( 𝑥𝐴 ∅ = ∅ → 𝐴 ≠ ∅)

Theoremintv 3951 The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.)
V = ∅

Theoremaxpweq 3952* Two equivalent ways to express the Power Set Axiom. Note that ax-pow 3955 is not used by the proof. (Contributed by NM, 22-Jun-2009.)
𝐴 ∈ V       (𝒫 𝐴 ∈ V ↔ ∃𝑥𝑦(∀𝑧(𝑧𝑦𝑧𝐴) → 𝑦𝑥))

2.2.6  Collection principle

Theorembnd 3953* A very strong generalization of the Axiom of Replacement (compare zfrep6 3902). 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 3900. (Contributed by NM, 17-Oct-2004.)
(∀𝑥𝑧𝑦𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑)

Theorembnd2 3954* A variant of the Boundedness Axiom bnd 3953 that picks a subset 𝑧 out of a possibly proper class 𝐵 in which a property is true. (Contributed by NM, 4-Feb-2004.)
𝐴 ∈ V       (∀𝑥𝐴𝑦𝐵 𝜑 → ∃𝑧(𝑧𝐵 ∧ ∀𝑥𝐴𝑦𝑧 𝜑))

2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing

2.3.1  Introduce the Axiom of Power Sets

Axiomax-pow 3955* 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 3906).

The variant axpow2 3957 uses explicit subset notation. A version using class notation is pwex 3960. (Contributed by NM, 5-Aug-1993.)

𝑦𝑧(∀𝑤(𝑤𝑧𝑤𝑥) → 𝑧𝑦)

Theoremzfpow 3956* Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
𝑥𝑦(∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦𝑥)

Theoremaxpow2 3957* A variant of the Axiom of Power Sets ax-pow 3955 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
𝑦𝑧(𝑧𝑥𝑧𝑦)

Theoremaxpow3 3958* A variant of the Axiom of Power Sets ax-pow 3955. 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.)
𝑦𝑧(𝑧𝑥𝑧𝑦)

Theoremel 3959* Every set is an element of some other set. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
𝑦 𝑥𝑦

Theorempwex 3960 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.)
𝐴 ∈ V       𝒫 𝐴 ∈ V

Theorempwexg 3961 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.)
(𝐴𝑉 → 𝒫 𝐴 ∈ V)

Theoremabssexg 3962* Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(𝐴𝑉 → {𝑥 ∣ (𝑥𝐴𝜑)} ∈ V)

TheoremsnexgOLD 3963 A singleton whose element exists is a set. The 𝐴 ∈ V 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 3964 and new proofs should use snexg 3964 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of snexg 3964 and then remove it.
(𝐴 ∈ V → {𝐴} ∈ V)

Theoremsnexg 3964 A singleton whose element exists is a set. The 𝐴 ∈ V 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.)
(𝐴𝑉 → {𝐴} ∈ V)

Theoremsnex 3965 A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
𝐴 ∈ V       {𝐴} ∈ V

Theoremsnexprc 3966 A singleton whose element is a proper class is a set. The ¬ 𝐴 ∈ V 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.)
𝐴 ∈ V → {𝐴} ∈ V)

Theoremp0ex 3967 The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.)
{∅} ∈ V

Theorempp0ex 3968 {∅, {∅}} (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.)
{∅, {∅}} ∈ V

Theoremord3ex 3969 The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.)
{∅, {∅}, {∅, {∅}}} ∈ V

Theoremdtruarb 3970* 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 4311 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.)
𝑥𝑦 ¬ 𝑥 = 𝑦

Theorempwuni 3971 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.)
𝐴 ⊆ 𝒫 𝐴

2.3.2  Axiom of Pairing

Axiomax-pr 3972* 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 3906). (Contributed by NM, 14-Nov-2006.)
𝑧𝑤((𝑤 = 𝑥𝑤 = 𝑦) → 𝑤𝑧)

Theoremzfpair2 3973 Derive the abbreviated version of the Axiom of Pairing from ax-pr 3972. (Contributed by NM, 14-Nov-2006.)
{𝑥, 𝑦} ∈ V

TheoremprexgOLD 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 3508, prprc1 3506, and prprc2 3507. This is a special case of prexg 3975 and new proofs should use prexg 3975 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of prexg 3975 and then remove it.
((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)

Theoremprexg 3975 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 3508, prprc1 3506, and prprc2 3507. (Contributed by Jim Kingdon, 16-Sep-2018.)
((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ V)

Theoremsnelpwi 3976 A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)
(𝐴𝐵 → {𝐴} ∈ 𝒫 𝐵)

Theoremsnelpw 3977 A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.)
𝐴 ∈ V       (𝐴𝐵 ↔ {𝐴} ∈ 𝒫 𝐵)

Theoremprelpwi 3978 A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.)
((𝐴𝐶𝐵𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)

Theoremrext 3979* A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.)
(∀𝑧(𝑥𝑧𝑦𝑧) → 𝑥 = 𝑦)

Theoremsspwb 3980 Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
(𝐴𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theoremunipw 3981 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.)
𝒫 𝐴 = 𝐴

Theorempwel 3982 Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.)
(𝐴𝐵 → 𝒫 𝐴 ∈ 𝒫 𝒫 𝐵)

Theorempwtr 3983 A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.)
(Tr 𝐴 ↔ Tr 𝒫 𝐴)

Theoremssextss 3984* An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.)
(𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))

Theoremssext 3985* 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.)
(𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))

Theoremnssssr 3986* Negation of subclass relationship. Compare nssr 3031. (Contributed by Jim Kingdon, 17-Sep-2018.)
(∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵) → ¬ 𝐴𝐵)

Theorempweqb 3987 Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
(𝐴 = 𝐵 ↔ 𝒫 𝐴 = 𝒫 𝐵)

Theoremintid 3988* The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.)
𝐴 ∈ V        {𝑥𝐴𝑥} = {𝐴}

Theoremeuabex 3989 The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.)
(∃!𝑥𝜑 → {𝑥𝜑} ∈ V)

Theoremmss 3990* An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.)
(∃𝑦 𝑦𝐴 → ∃𝑥(𝑥𝐴 ∧ ∃𝑧 𝑧𝑥))

Theoremexss 3991* Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.)
(∃𝑥𝐴 𝜑 → ∃𝑦(𝑦𝐴 ∧ ∃𝑥𝑦 𝜑))

Theoremopexg 3992 An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)
((𝐴𝑉𝐵𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

TheoremopexgOLD 3993 An ordered pair of sets is a set. This is a special case of opexg 3992 and new proofs should use opexg 3992 instead. (Contributed by Jim Kingdon, 19-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of opexg 3992 and then remove it.
((𝐴 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐴, 𝐵⟩ ∈ V)

Theoremopex 3994 An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.)
𝐴 ∈ V    &   𝐵 ∈ V       𝐴, 𝐵⟩ ∈ V

Theoremotexg 3995 An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.)
((𝐴𝑈𝐵𝑉𝐶𝑊) → ⟨𝐴, 𝐵, 𝐶⟩ ∈ V)

Theoremelop 3996 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.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V       (𝐴 ∈ ⟨𝐵, 𝐶⟩ ↔ (𝐴 = {𝐵} ∨ 𝐴 = {𝐵, 𝐶}))

Theoremopi1 3997 One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V       {𝐴} ∈ ⟨𝐴, 𝐵

Theoremopi2 3998 One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V       {𝐴, 𝐵} ∈ ⟨𝐴, 𝐵

2.3.3  Ordered pair theorem

Theoremopm 3999* An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.)
(∃𝑥 𝑥 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))

Theoremopnzi 4000 An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3999). (Contributed by Mario Carneiro, 26-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V       𝐴, 𝐵⟩ ≠ ∅

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10511
 Copyright terms: Public domain < Previous  Next >