Home | Intuitionistic Logic Explorer Theorem List (p. 40 of 94) | < 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 | elpw2g 3901 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
⊢ (B ∈ 𝑉 → (A ∈ 𝒫 B ↔ A ⊆ B)) | ||
Theorem | elpw2 3902 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
⊢ B ∈ V ⇒ ⊢ (A ∈ 𝒫 B ↔ A ⊆ B) | ||
Theorem | pwnss 3903 | The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (A ∈ 𝑉 → ¬ 𝒫 A ⊆ A) | ||
Theorem | pwne 3904 | No set equals its power set. The sethood antecedent is necessary; compare pwv 3570. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ (A ∈ 𝑉 → 𝒫 A ≠ A) | ||
Theorem | repizf2lem 3905 | Lemma for repizf2 3906. If we have a function-like proposition which provides at most one value of y for each x in a set w, we can change "at most one" to "exactly one" by restricting the values of x to those values for which the proposition provides a value of y. (Contributed by Jim Kingdon, 7-Sep-2018.) |
⊢ (∀x ∈ w ∃*yφ ↔ ∀x ∈ {x ∈ w ∣ ∃yφ}∃!yφ) | ||
Theorem | repizf2 3906* | Replacement. This version of replacement is stronger than repizf 3864 in the sense that φ does not need to map all values of x in w to a value of y. The resulting set contains those elements for which there is a value of y and in that sense, this theorem combines repizf 3864 with ax-sep 3866. Another variation would be ∀x ∈ w∃*yφ → {y ∣ ∃x(x ∈ w ∧ φ)} ∈ V but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.) |
⊢ Ⅎzφ ⇒ ⊢ (∀x ∈ w ∃*yφ → ∃z∀x ∈ {x ∈ w ∣ ∃yφ}∃y ∈ z φ) | ||
Theorem | class2seteq 3907* | Equality theorem for classes and sets . (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |
⊢ (A ∈ 𝑉 → {x ∈ A ∣ A ∈ V} = A) | ||
Theorem | 0elpw 3908 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |
⊢ ∅ ∈ 𝒫 A | ||
Theorem | 0nep0 3909 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |
⊢ ∅ ≠ {∅} | ||
Theorem | 0inp0 3910 | Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 30-Sep-2003.) |
⊢ (A = ∅ → ¬ A = {∅}) | ||
Theorem | unidif0 3911 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |
⊢ ∪ (A ∖ {∅}) = ∪ A | ||
Theorem | iin0imm 3912* | An indexed intersection of the empty set, with an inhabited index set, is empty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
⊢ (∃y y ∈ A → ∩ x ∈ A ∅ = ∅) | ||
Theorem | iin0r 3913* | If an indexed intersection of the empty set is empty, the index set is non-empty. (Contributed by Jim Kingdon, 29-Aug-2018.) |
⊢ (∩ x ∈ A ∅ = ∅ → A ≠ ∅) | ||
Theorem | intv 3914 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |
⊢ ∩ V = ∅ | ||
Theorem | axpweq 3915* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 3918 is not used by the proof. (Contributed by NM, 22-Jun-2009.) |
⊢ A ∈ V ⇒ ⊢ (𝒫 A ∈ V ↔ ∃x∀y(∀z(z ∈ y → z ∈ A) → y ∈ x)) | ||
Theorem | bnd 3916* | A very strong generalization of the Axiom of Replacement (compare zfrep6 3865). Its strength lies in the rather profound fact that φ(x, y) 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 3863. (Contributed by NM, 17-Oct-2004.) |
⊢ (∀x ∈ z ∃yφ → ∃w∀x ∈ z ∃y ∈ w φ) | ||
Theorem | bnd2 3917* | A variant of the Boundedness Axiom bnd 3916 that picks a subset z out of a possibly proper class B in which a property is true. (Contributed by NM, 4-Feb-2004.) |
⊢ A ∈ V ⇒ ⊢ (∀x ∈ A ∃y ∈ B φ → ∃z(z ⊆ B ∧ ∀x ∈ A ∃y ∈ z φ)) | ||
Axiom | ax-pow 3918* |
Axiom of Power Sets. An axiom of Intuitionistic Zermelo-Fraenkel set
theory. It states that a set y exists that includes the power set
of a given set x i.e. contains every subset of x. 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 3869).
The variant axpow2 3920 uses explicit subset notation. A version using class notation is pwex 3923. (Contributed by NM, 5-Aug-1993.) |
⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y) | ||
Theorem | zfpow 3919* | Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
⊢ ∃x∀y(∀x(x ∈ y → x ∈ z) → y ∈ x) | ||
Theorem | axpow2 3920* | A variant of the Axiom of Power Sets ax-pow 3918 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃y∀z(z ⊆ x → z ∈ y) | ||
Theorem | axpow3 3921* | A variant of the Axiom of Power Sets ax-pow 3918. For any set x, there exists a set y whose members are exactly the subsets of x i.e. the power set of x. Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃y∀z(z ⊆ x ↔ z ∈ y) | ||
Theorem | el 3922* | Every set is an element of some other set. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ∃y x ∈ y | ||
Theorem | pwex 3923 | 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.) |
⊢ A ∈ V ⇒ ⊢ 𝒫 A ∈ V | ||
Theorem | pwexg 3924 | 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.) |
⊢ (A ∈ 𝑉 → 𝒫 A ∈ V) | ||
Theorem | abssexg 3925* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (A ∈ 𝑉 → {x ∣ (x ⊆ A ∧ φ)} ∈ V) | ||
Theorem | snexgOLD 3926 | A singleton whose element exists is a set. The A ∈ 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 3927 and new proofs should use snexg 3927 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of snexg 3927 and then remove it. |
⊢ (A ∈ V → {A} ∈ V) | ||
Theorem | snexg 3927 | A singleton whose element exists is a set. The A ∈ 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.) |
⊢ (A ∈ 𝑉 → {A} ∈ V) | ||
Theorem | snex 3928 | A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ A ∈ V ⇒ ⊢ {A} ∈ V | ||
Theorem | snexprc 3929 | A singleton whose element is a proper class is a set. The ¬ A ∈ 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.) |
⊢ (¬ A ∈ V → {A} ∈ V) | ||
Theorem | p0ex 3930 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |
⊢ {∅} ∈ V | ||
Theorem | pp0ex 3931 | {∅, {∅}} (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |
⊢ {∅, {∅}} ∈ V | ||
Theorem | ord3ex 3932 | The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.) |
⊢ {∅, {∅}, {∅, {∅}}} ∈ V | ||
Theorem | dtruarb 3933* | 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 4237 in which we are given a set y and go from there to a set x which is not equal to it. (Contributed by Jim Kingdon, 2-Sep-2018.) |
⊢ ∃x∃y ¬ x = y | ||
Theorem | pwuni 3934 | 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.) |
⊢ A ⊆ 𝒫 ∪ A | ||
Axiom | ax-pr 3935* | 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 3869). (Contributed by NM, 14-Nov-2006.) |
⊢ ∃z∀w((w = x ∨ w = y) → w ∈ z) | ||
Theorem | zfpair2 3936 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 3935. (Contributed by NM, 14-Nov-2006.) |
⊢ {x, y} ∈ V | ||
Theorem | prexgOLD 3937 | 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 3471, prprc1 3469, and prprc2 3470. This is a special case of prexg 3938 and new proofs should use prexg 3938 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of prexg 3938 and then remove it. |
⊢ ((A ∈ V ∧ B ∈ V) → {A, B} ∈ V) | ||
Theorem | prexg 3938 | 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 3471, prprc1 3469, and prprc2 3470. (Contributed by Jim Kingdon, 16-Sep-2018.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → {A, B} ∈ V) | ||
Theorem | snelpwi 3939 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.) |
⊢ (A ∈ B → {A} ∈ 𝒫 B) | ||
Theorem | snelpw 3940 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |
⊢ A ∈ V ⇒ ⊢ (A ∈ B ↔ {A} ∈ 𝒫 B) | ||
Theorem | prelpwi 3941 | A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.) |
⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐶) → {A, B} ∈ 𝒫 𝐶) | ||
Theorem | rext 3942* | A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.) |
⊢ (∀z(x ∈ z → y ∈ z) → x = y) | ||
Theorem | sspwb 3943 | Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
⊢ (A ⊆ B ↔ 𝒫 A ⊆ 𝒫 B) | ||
Theorem | unipw 3944 | 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.) |
⊢ ∪ 𝒫 A = A | ||
Theorem | pwel 3945 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |
⊢ (A ∈ B → 𝒫 A ∈ 𝒫 𝒫 ∪ B) | ||
Theorem | pwtr 3946 | 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 A ↔ Tr 𝒫 A) | ||
Theorem | ssextss 3947* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
⊢ (A ⊆ B ↔ ∀x(x ⊆ A → x ⊆ B)) | ||
Theorem | ssext 3948* | 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.) |
⊢ (A = B ↔ ∀x(x ⊆ A ↔ x ⊆ B)) | ||
Theorem | nssssr 3949* | Negation of subclass relationship. Compare nssr 2997. (Contributed by Jim Kingdon, 17-Sep-2018.) |
⊢ (∃x(x ⊆ A ∧ ¬ x ⊆ B) → ¬ A ⊆ B) | ||
Theorem | pweqb 3950 | Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
⊢ (A = B ↔ 𝒫 A = 𝒫 B) | ||
Theorem | intid 3951* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |
⊢ A ∈ V ⇒ ⊢ ∩ {x ∣ A ∈ x} = {A} | ||
Theorem | euabex 3952 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
⊢ (∃!xφ → {x ∣ φ} ∈ V) | ||
Theorem | mss 3953* | An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.) |
⊢ (∃y y ∈ A → ∃x(x ⊆ A ∧ ∃z z ∈ x)) | ||
Theorem | exss 3954* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
⊢ (∃x ∈ A φ → ∃y(y ⊆ A ∧ ∃x ∈ y φ)) | ||
Theorem | opexg 3955 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ⟨A, B⟩ ∈ V) | ||
Theorem | opexgOLD 3956 | An ordered pair of sets is a set. This is a special case of opexg 3955 and new proofs should use opexg 3955 instead. (Contributed by Jim Kingdon, 19-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of opexg 3955 and then remove it. |
⊢ ((A ∈ V ∧ B ∈ V) → ⟨A, B⟩ ∈ V) | ||
Theorem | opex 3957 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ⟨A, B⟩ ∈ V | ||
Theorem | otexg 3958 | An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.) |
⊢ ((A ∈ 𝑈 ∧ B ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ⟨A, B, 𝐶⟩ ∈ V) | ||
Theorem | elop 3959 | 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.) |
⊢ A ∈ V & ⊢ B ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (A ∈ ⟨B, 𝐶⟩ ↔ (A = {B} ∨ A = {B, 𝐶})) | ||
Theorem | opi1 3960 | One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ {A} ∈ ⟨A, B⟩ | ||
Theorem | opi2 3961 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ {A, B} ∈ ⟨A, B⟩ | ||
Theorem | opm 3962* | An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.) |
⊢ (∃x x ∈ ⟨A, B⟩ ↔ (A ∈ V ∧ B ∈ V)) | ||
Theorem | opnzi 3963 | An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 3962). (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ⟨A, B⟩ ≠ ∅ | ||
Theorem | opth1 3964 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ → A = 𝐶) | ||
Theorem | opth 3965 | 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.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 ∧ B = 𝐷)) | ||
Theorem | opthg 3966 | 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.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 ∧ B = 𝐷))) | ||
Theorem | opthg2 3967 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 ∧ B = 𝐷))) | ||
Theorem | opth2 3968 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ ↔ (A = 𝐶 ∧ B = 𝐷)) | ||
Theorem | otth2 3969 | Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V & ⊢ B ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (⟨⟨A, B⟩, 𝑅⟩ = ⟨⟨𝐶, 𝐷⟩, 𝑆⟩ ↔ (A = 𝐶 ∧ B = 𝐷 ∧ 𝑅 = 𝑆)) | ||
Theorem | otth 3970 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V & ⊢ B ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (⟨A, B, 𝑅⟩ = ⟨𝐶, 𝐷, 𝑆⟩ ↔ (A = 𝐶 ∧ B = 𝐷 ∧ 𝑅 = 𝑆)) | ||
Theorem | eqvinop 3971* | A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
⊢ B ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (A = ⟨B, 𝐶⟩ ↔ ∃x∃y(A = ⟨x, y⟩ ∧ ⟨x, y⟩ = ⟨B, 𝐶⟩)) | ||
Theorem | copsexg 3972* | Substitution of class A for ordered pair ⟨x, y⟩. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (A = ⟨x, y⟩ → (φ ↔ ∃x∃y(A = ⟨x, y⟩ ∧ φ))) | ||
Theorem | copsex2t 3973* | Closed theorem form of copsex2g 3974. (Contributed by NM, 17-Feb-2013.) |
⊢ ((∀x∀y((x = A ∧ y = B) → (φ ↔ ψ)) ∧ (A ∈ 𝑉 ∧ B ∈ 𝑊)) → (∃x∃y(⟨A, B⟩ = ⟨x, y⟩ ∧ φ) ↔ ψ)) | ||
Theorem | copsex2g 3974* | Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) |
⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (∃x∃y(⟨A, B⟩ = ⟨x, y⟩ ∧ φ) ↔ ψ)) | ||
Theorem | copsex4g 3975* | An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.) |
⊢ (((x = A ∧ y = B) ∧ (z = 𝐶 ∧ w = 𝐷)) → (φ ↔ ψ)) ⇒ ⊢ (((A ∈ 𝑅 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃x∃y∃z∃w((⟨A, B⟩ = ⟨x, y⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨z, w⟩) ∧ φ) ↔ ψ)) | ||
Theorem | 0nelop 3976 | A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ¬ ∅ ∈ ⟨A, B⟩ | ||
Theorem | opeqex 3977 | Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.) |
⊢ (⟨A, B⟩ = ⟨𝐶, 𝐷⟩ → ((A ∈ V ∧ B ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V))) | ||
Theorem | opcom 3978 | An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩ = ⟨B, A⟩ ↔ A = B) | ||
Theorem | moop2 3979* | "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ B ∈ V ⇒ ⊢ ∃*x A = ⟨B, x⟩ | ||
Theorem | opeqsn 3980 | Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) |
⊢ A ∈ V & ⊢ B ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (⟨A, B⟩ = {𝐶} ↔ (A = B ∧ 𝐶 = {A})) | ||
Theorem | opeqpr 3981 | Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) |
⊢ A ∈ V & ⊢ B ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (⟨A, B⟩ = {𝐶, 𝐷} ↔ ((𝐶 = {A} ∧ 𝐷 = {A, B}) ∨ (𝐶 = {A, B} ∧ 𝐷 = {A}))) | ||
Theorem | euotd 3982* | Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.) |
⊢ (φ → A ∈ V) & ⊢ (φ → B ∈ V) & ⊢ (φ → 𝐶 ∈ V) & ⊢ (φ → (ψ ↔ (𝑎 = A ∧ 𝑏 = B ∧ 𝑐 = 𝐶))) ⇒ ⊢ (φ → ∃!x∃𝑎∃𝑏∃𝑐(x = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ψ)) | ||
Theorem | uniop 3983 | The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ∪ ⟨A, B⟩ = {A, B} | ||
Theorem | uniopel 3984 | Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩ ∈ 𝐶 → ∪ ⟨A, B⟩ ∈ ∪ 𝐶) | ||
Theorem | opabid 3985 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (⟨x, y⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ φ) | ||
Theorem | elopab 3986* | Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.) |
⊢ (A ∈ {⟨x, y⟩ ∣ φ} ↔ ∃x∃y(A = ⟨x, y⟩ ∧ φ)) | ||
Theorem | opelopabsbALT 3987* | The law of concretion in terms of substitutions. Less general than opelopabsb 3988, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (⟨z, w⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [w / y][z / x]φ) | ||
Theorem | opelopabsb 3988* | The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ [A / x][B / y]φ) | ||
Theorem | brabsb 3989* | The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.) |
⊢ 𝑅 = {⟨x, y⟩ ∣ φ} ⇒ ⊢ (A𝑅B ↔ [A / x][B / y]φ) | ||
Theorem | opelopabt 3990* | Closed theorem form of opelopab 3999. (Contributed by NM, 19-Feb-2013.) |
⊢ ((∀x∀y(x = A → (φ ↔ ψ)) ∧ ∀x∀y(y = B → (ψ ↔ χ)) ∧ (A ∈ 𝑉 ∧ B ∈ 𝑊)) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ χ)) | ||
Theorem | opelopabga 3991* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ ψ)) | ||
Theorem | brabga 3992* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) & ⊢ 𝑅 = {⟨x, y⟩ ∣ φ} ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A𝑅B ↔ ψ)) | ||
Theorem | opelopab2a 3993* | Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ ((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧ φ)} ↔ ψ)) | ||
Theorem | opelopaba 3994* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ A ∈ V & ⊢ B ∈ V & ⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) ⇒ ⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ ψ) | ||
Theorem | braba 3995* | The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.) |
⊢ A ∈ V & ⊢ B ∈ V & ⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) & ⊢ 𝑅 = {⟨x, y⟩ ∣ φ} ⇒ ⊢ (A𝑅B ↔ ψ) | ||
Theorem | opelopabg 3996* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ χ)) | ||
Theorem | brabg 3997* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) & ⊢ 𝑅 = {⟨x, y⟩ ∣ φ} ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (A𝑅B ↔ χ)) | ||
Theorem | opelopab2 3998* | Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ ((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧ φ)} ↔ χ)) | ||
Theorem | opelopab 3999* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.) |
⊢ A ∈ V & ⊢ B ∈ V & ⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) ⇒ ⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ χ) | ||
Theorem | brab 4000* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) |
⊢ A ∈ V & ⊢ B ∈ V & ⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) & ⊢ 𝑅 = {⟨x, y⟩ ∣ φ} ⇒ ⊢ (A𝑅B ↔ χ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |