Home | Intuitionistic Logic Explorer Theorem List (p. 40 of 108) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ax9vsep 3901* | Derive a weakened version of ax-9 1464, where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 3896 and Extensionality ax-ext 2063. In intuitionistic logic a9evsep 3900 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | zfnuleu 3902* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2066 to strengthen the hypothesis in the form of axnul 3903). (Contributed by NM, 22-Dec-2007.) |
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 ⇒ ⊢ ∃!𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | ||
Theorem | axnul 3903* |
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 3896. 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 3902).
This theorem should not be referenced by any proof. Instead, use ax-nul 3904 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 3904* | The Null Set Axiom of IZF set theory. It was derived as axnul 3903 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 3905 | 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 3904. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ ∅ ∈ V | ||
Theorem | csbexga 3906 | The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → ⦋𝐴 / 𝑥⦌𝐵 ∈ V) | ||
Theorem | csbexa 3907 | 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 | ||
Theorem | nalset 3908* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥 | ||
Theorem | vprc 3909 | 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 | ||
Theorem | nvel 3910 | The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.) |
⊢ ¬ V ∈ 𝐴 | ||
Theorem | vnex 3911 | The universal class does not exist. (Contributed by NM, 4-Jul-2005.) |
⊢ ¬ ∃𝑥 𝑥 = V | ||
Theorem | inex1 3912 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∩ 𝐵) ∈ V | ||
Theorem | inex2 3913 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∩ 𝐴) ∈ V | ||
Theorem | inex1g 3914 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V) | ||
Theorem | ssex 3915 | 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 3896 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) | ||
Theorem | ssexi 3916 | The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
⊢ 𝐵 ∈ V & ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | ssexg 3917 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | ssexd 3918 | A subclass of a set is a set. Deduction form of ssexg 3917. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ V) | ||
Theorem | difexg 3919 | Existence of a difference. (Contributed by NM, 26-May-1998.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V) | ||
Theorem | zfausab 3920* | Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | rabexg 3921* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | ||
Theorem | rabex 3922* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V | ||
Theorem | elssabg 3923* | Membership in a class abstraction involving a subset. Unlike elabg 2739, 𝐴 does not have to be a set. (Contributed by NM, 29-Aug-2006.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝜑)} ↔ (𝐴 ⊆ 𝐵 ∧ 𝜓))) | ||
Theorem | inteximm 3924* | The intersection of an inhabited class exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) | ||
Theorem | intexr 3925 | If the intersection of a class exists, the class is non-empty. (Contributed by Jim Kingdon, 27-Aug-2018.) |
⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅) | ||
Theorem | intnexr 3926 | 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) | ||
Theorem | intexabim 3927 | The intersection of an inhabited class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
⊢ (∃𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} ∈ V) | ||
Theorem | intexrabim 3928 | The intersection of an inhabited restricted class abstraction exists. (Contributed by Jim Kingdon, 27-Aug-2018.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∩ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | ||
Theorem | iinexgm 3929* | 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) | ||
Theorem | inuni 3930* | 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 3931 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpw2 3932 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
Theorem | pwnss 3933 | The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝐴 ∈ 𝑉 → ¬ 𝒫 𝐴 ⊆ 𝐴) | ||
Theorem | pwne 3934 | No set equals its power set. The sethood antecedent is necessary; compare pwv 3600. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ≠ 𝐴) | ||
Theorem | repizf2lem 3935 | Lemma for repizf2 3936. 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 3936* | Replacement. This version of replacement is stronger than repizf 3894 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 3894 with ax-sep 3896. Another variation would be ∀𝑥 ∈ 𝑤∃*𝑦𝜑 → {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)} ∈ V but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝑤 ∃*𝑦𝜑 → ∃𝑧∀𝑥 ∈ {𝑥 ∈ 𝑤 ∣ ∃𝑦𝜑}∃𝑦 ∈ 𝑧 𝜑) | ||
Theorem | class2seteq 3937* | Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V} = 𝐴) | ||
Theorem | 0elpw 3938 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
⊢ ∅ ∈ 𝒫 𝐴 | ||
Theorem | 0nep0 3939 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |
⊢ ∅ ≠ {∅} | ||
Theorem | 0inp0 3940 | 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 3941 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |
⊢ ∪ (𝐴 ∖ {∅}) = ∪ 𝐴 | ||
Theorem | iin0imm 3942* | An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ∅ = ∅) | ||
Theorem | iin0r 3943* | 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 3944 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |
⊢ ∩ V = ∅ | ||
Theorem | axpweq 3945* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 3948 is not used by the proof. (Contributed by NM, 22-Jun-2009.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝒫 𝐴 ∈ V ↔ ∃𝑥∀𝑦(∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝑥)) | ||
Theorem | bnd 3946* | A very strong generalization of the Axiom of Replacement (compare zfrep6 3895). 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 3893. (Contributed by NM, 17-Oct-2004.) |
⊢ (∀𝑥 ∈ 𝑧 ∃𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) | ||
Theorem | bnd2 3947* | A variant of the Boundedness Axiom bnd 3946 that picks a subset 𝑧 out of a possibly proper class 𝐵 in which a property is true. (Contributed by NM, 4-Feb-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑)) | ||
Axiom | ax-pow 3948* |
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 3899).
The variant axpow2 3950 uses explicit subset notation. A version using class notation is pwex 3953. (Contributed by NM, 5-Aug-1993.) |
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfpow 3949* | Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
⊢ ∃𝑥∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axpow2 3950* | A variant of the Axiom of Power Sets ax-pow 3948 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦) | ||
Theorem | axpow3 3951* | A variant of the Axiom of Power Sets ax-pow 3948. 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 3952* | 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 3953 | 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 | ||
Theorem | pwexg 3954 | 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) | ||
Theorem | abssexg 3955* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V) | ||
Theorem | snexg 3956 | 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) | ||
Theorem | snex 3957 | A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ∈ V | ||
Theorem | snexprc 3958 | 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) | ||
Theorem | p0ex 3959 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |
⊢ {∅} ∈ V | ||
Theorem | pp0ex 3960 | {∅, {∅}} (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |
⊢ {∅, {∅}} ∈ V | ||
Theorem | ord3ex 3961 | The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.) |
⊢ {∅, {∅}, {∅, {∅}}} ∈ V | ||
Theorem | dtruarb 3962* | 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 4302 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 3963 | 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 3964* | 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 3899). (Contributed by NM, 14-Nov-2006.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Theorem | zfpair2 3965 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 3964. (Contributed by NM, 14-Nov-2006.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | prexg 3966 | 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 3502, prprc1 3500, and prprc2 3501. (Contributed by Jim Kingdon, 16-Sep-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) | ||
Theorem | snelpwi 3967 | 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 3968 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | prelpwi 3969 | 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 3970* | 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 3971 | 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 3972 | 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 3973 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |
⊢ (𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝒫 𝒫 ∪ 𝐵) | ||
Theorem | pwtr 3974 | 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 𝒫 𝐴) | ||
Theorem | ssextss 3975* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) | ||
Theorem | ssext 3976* | 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 3977* | Negation of subclass relationship. Compare nssr 3057. (Contributed by Jim Kingdon, 17-Sep-2018.) |
⊢ (∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐵) | ||
Theorem | pweqb 3978 | 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 3979* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴} | ||
Theorem | euabex 3980 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V) | ||
Theorem | mss 3981* | An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ ∃𝑧 𝑧 ∈ 𝑥)) | ||
Theorem | exss 3982* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑)) | ||
Theorem | opexg 3983 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 ∈ V) | ||
Theorem | opex 3984 | 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 | ||
Theorem | otexg 3985 | An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → 〈𝐴, 𝐵, 𝐶〉 ∈ V) | ||
Theorem | elop 3986 | 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 ⇒ ⊢ (𝐴 ∈ 〈𝐵, 𝐶〉 ↔ (𝐴 = {𝐵} ∨ 𝐴 = {𝐵, 𝐶})) | ||
Theorem | opi1 3987 | One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 | ||
Theorem | opi2 3988 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝐴, 𝐵} ∈ 〈𝐴, 𝐵〉 | ||
Theorem | opm 3989* | An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.) |
⊢ (∃𝑥 𝑥 ∈ 〈𝐴, 𝐵〉 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | opnzi 3990 | An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3989). (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ 〈𝐴, 𝐵〉 ≠ ∅ | ||
Theorem | opth1 3991 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) | ||
Theorem | opth 3992 | 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.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthg 3993 | 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 3994 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | opth2 3995 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | otth2 3996 | Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (〈〈𝐴, 𝐵〉, 𝑅〉 = 〈〈𝐶, 𝐷〉, 𝑆〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) | ||
Theorem | otth 3997 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (〈𝐴, 𝐵, 𝑅〉 = 〈𝐶, 𝐷, 𝑆〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) | ||
Theorem | eqvinop 3998* | A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 = 〈𝐵, 𝐶〉 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 = 〈𝐵, 𝐶〉)) | ||
Theorem | copsexg 3999* | Substitution of class 𝐴 for ordered pair 〈𝑥, 𝑦〉. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | ||
Theorem | copsex2t 4000* | Closed theorem form of copsex2g 4001. (Contributed by NM, 17-Feb-2013.) |
⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |