Home | Intuitionistic Logic Explorer Theorem List (p. 42 of 133) | < 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 | axpow3 4101* | A variant of the Axiom of Power Sets ax-pow 4098. 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 4102* | 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 4103 | 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 4104 from vpwex 4103. (Revised by BJ, 10-Aug-2022.) |
⊢ 𝒫 𝑥 ∈ V | ||
Theorem | pwexg 4104 | Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | ||
Theorem | pwexd 4105 | Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ∈ V) | ||
Theorem | abssexg 4106* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V) | ||
Theorem | pwex 4107 | Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝒫 𝐴 ∈ V | ||
Theorem | snexg 4108 | 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 4109 | 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 4110 | 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 | notnotsnex 4111 | A singleton is never a proper class. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jul-2022.) |
⊢ ¬ ¬ {𝐴} ∈ V | ||
Theorem | p0ex 4112 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |
⊢ {∅} ∈ V | ||
Theorem | pp0ex 4113 | {∅, {∅}} (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |
⊢ {∅, {∅}} ∈ V | ||
Theorem | ord3ex 4114 | The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.) |
⊢ {∅, {∅}, {∅, {∅}}} ∈ V | ||
Theorem | dtruarb 4115* | 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 4474 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 4116 | 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 | undifexmid 4117* | Union of complementary parts producing the whole and excluded middle. Although special cases such as undifss 3443 and undifdcss 6811 are provable, the full statement implies excluded middle as shown here. (Contributed by Jim Kingdon, 16-Jun-2022.) |
⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Syntax | wem 4118 | Formula for an abbreviation of excluded middle. |
wff EXMID | ||
Definition | df-exmid 4119 |
The expression EXMID will be used as a
readable shorthand for any
form of the law of the excluded middle; this is a useful shorthand
largely because it hides statements of the form "for any
proposition" in
a system which can only quantify over sets, not propositions.
To see how this compares with other ways of expressing excluded middle, compare undifexmid 4117 with exmidundif 4129. The former may be more recognizable as excluded middle because it is in terms of propositions, and the proof may be easier to follow for much the same reason (it just has to show 𝜑 and ¬ 𝜑 in the the relevant parts of the proof). The latter, however, has the key advantage of being able to prove both directions of the biconditional. To state that excluded middle implies a proposition is hard to do gracefully without EXMID, because there is no way to write a hypothesis 𝜑 ∨ ¬ 𝜑 for an arbitrary proposition; instead the hypothesis would need to be the particular instance of excluded middle which that proof needs. Or to say it another way, EXMID implies DECID 𝜑 by exmidexmid 4120 but there is no good way to express the converse. This definition and how we use it is easiest to understand (and most appropriate to assign the name "excluded middle" to) if we assume ax-sep 4046, in which case EXMID means that all propositions are decidable (see exmidexmid 4120 and notice that it relies on ax-sep 4046). If we instead work with ax-bdsep 13082, EXMID as defined here means that all bounded propositions are decidable. (Contributed by Mario Carneiro and Jim Kingdon, 18-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥)) | ||
Theorem | exmidexmid 4120 |
EXMID implies that an arbitrary proposition is decidable. That is,
EXMID captures the usual meaning of excluded middle when stated in terms
of propositions.
To get other propositional statements which are equivalent to excluded middle, combine this with notnotrdc 828, peircedc 899, or condc 838. (Contributed by Jim Kingdon, 18-Jun-2022.) |
⊢ (EXMID → DECID 𝜑) | ||
Theorem | exmid01 4121 | Excluded middle is equivalent to saying any subset of {∅} is either ∅ or {∅}. (Contributed by BJ and Jim Kingdon, 18-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) | ||
Theorem | pwntru 4122 | A slight strengthening of pwtrufal 13192. (Contributed by Mario Carneiro and Jim Kingdon, 12-Sep-2023.) |
⊢ ((𝐴 ⊆ {∅} ∧ 𝐴 ≠ {∅}) → 𝐴 = ∅) | ||
Theorem | exmid1dc 4123* | A convenience theorem for proving that something implies EXMID. Think of this as an alternative to using a proposition, as in proofs like undifexmid 4117 or ordtriexmid 4437. In this context 𝑥 = {∅} can be thought of as "x is true". (Contributed by Jim Kingdon, 21-Nov-2023.) |
⊢ ((𝜑 ∧ 𝑥 ⊆ {∅}) → DECID 𝑥 = {∅}) ⇒ ⊢ (𝜑 → EXMID) | ||
Theorem | exmidn0m 4124* | Excluded middle is equivalent to any set being empty or inhabited. (Contributed by Jim Kingdon, 5-Mar-2023.) |
⊢ (EXMID ↔ ∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥)) | ||
Theorem | exmidsssn 4125* | Excluded middle is equivalent to the biconditionalized version of sssnr 3680 for sets. (Contributed by Jim Kingdon, 5-Mar-2023.) |
⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ {𝑦} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑦}))) | ||
Theorem | exmidsssnc 4126* | Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4121 but lets you choose any set as the element of the singleton rather than just ∅. It is similar to exmidsssn 4125 but for a particular set 𝐵 rather than all sets. (Contributed by Jim Kingdon, 29-Jul-2023.) |
⊢ (𝐵 ∈ 𝑉 → (EXMID ↔ ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))) | ||
Theorem | exmid0el 4127 | Excluded middle is equivalent to decidability of ∅ being an element of an arbitrary set. (Contributed by Jim Kingdon, 18-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥DECID ∅ ∈ 𝑥) | ||
Theorem | exmidel 4128* | Excluded middle is equivalent to decidability of membership for two arbitrary sets. (Contributed by Jim Kingdon, 18-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥∀𝑦DECID 𝑥 ∈ 𝑦) | ||
Theorem | exmidundif 4129* | Excluded middle is equivalent to every subset having a complement. That is, the union of a subset and its relative complement being the whole set. Although special cases such as undifss 3443 and undifdcss 6811 are provable, the full statement is equivalent to excluded middle as shown here. (Contributed by Jim Kingdon, 18-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)) | ||
Theorem | exmidundifim 4130* | Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4129 with an implication rather than a biconditional. (Contributed by Jim Kingdon, 16-Feb-2023.) |
⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)) | ||
Axiom | ax-pr 4131* | 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 4049). (Contributed by NM, 14-Nov-2006.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Theorem | zfpair2 4132 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 4131. (Contributed by NM, 14-Nov-2006.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | prexg 4133 | 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 3633, prprc1 3631, and prprc2 3632. (Contributed by Jim Kingdon, 16-Sep-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) | ||
Theorem | snelpwi 4134 | 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 4135 | 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 4136 | 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 4137* | 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 4138 | 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 4139 | 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 4140 | Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) |
⊢ (𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝒫 𝒫 ∪ 𝐵) | ||
Theorem | pwtr 4141 | 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 4142* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) | ||
Theorem | ssext 4143* | 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 4144* | Negation of subclass relationship. Compare nssr 3157. (Contributed by Jim Kingdon, 17-Sep-2018.) |
⊢ (∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐵) | ||
Theorem | pweqb 4145 | 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 4146* | 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 4147 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V) | ||
Theorem | mss 4148* | An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ ∃𝑧 𝑧 ∈ 𝑥)) | ||
Theorem | exss 4149* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑)) | ||
Theorem | opexg 4150 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 ∈ V) | ||
Theorem | opex 4151 | 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 4152 | An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → 〈𝐴, 𝐵, 𝐶〉 ∈ V) | ||
Theorem | elop 4153 | 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 4154 | 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 4155 | 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 4156* | An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.) |
⊢ (∃𝑥 𝑥 ∈ 〈𝐴, 𝐵〉 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | opnzi 4157 | An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 4156). (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ 〈𝐴, 𝐵〉 ≠ ∅ | ||
Theorem | opth1 4158 | 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 4159 | 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 4160 | 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 4161 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | opth2 4162 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | otth2 4163 | 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 4164 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (〈𝐴, 𝐵, 𝑅〉 = 〈𝐶, 𝐷, 𝑆〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) | ||
Theorem | eqvinop 4165* | 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 4166* | Substitution of class 𝐴 for ordered pair 〈𝑥, 𝑦〉. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | ||
Theorem | copsex2t 4167* | Closed theorem form of copsex2g 4168. (Contributed by NM, 17-Feb-2013.) |
⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | copsex2g 4168* | Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | copsex4g 4169* | An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.) |
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤((〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑧, 𝑤〉) ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | 0nelop 4170 | A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ¬ ∅ ∈ 〈𝐴, 𝐵〉 | ||
Theorem | opeqex 4171 | Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.) |
⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V))) | ||
Theorem | opcom 4172 | An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐵, 𝐴〉 ↔ 𝐴 = 𝐵) | ||
Theorem | moop2 4173* | "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ∃*𝑥 𝐴 = 〈𝐵, 𝑥〉 | ||
Theorem | opeqsn 4174 | Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})) | ||
Theorem | opeqpr 4175 | Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = {𝐶, 𝐷} ↔ ((𝐶 = {𝐴} ∧ 𝐷 = {𝐴, 𝐵}) ∨ (𝐶 = {𝐴, 𝐵} ∧ 𝐷 = {𝐴}))) | ||
Theorem | euotd 4176* | Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶))) ⇒ ⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) | ||
Theorem | uniop 4177 | 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.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ 〈𝐴, 𝐵〉 = {𝐴, 𝐵} | ||
Theorem | uniopel 4178 | Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → ∪ 〈𝐴, 𝐵〉 ∈ ∪ 𝐶) | ||
Theorem | opabid 4179 | 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.) |
⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) | ||
Theorem | elopab 4180* | Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) | ||
Theorem | opelopabsbALT 4181* | The law of concretion in terms of substitutions. Less general than opelopabsb 4182, 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.) |
⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑) | ||
Theorem | opelopabsb 4182* | The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) | ||
Theorem | brabsb 4183* | The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) | ||
Theorem | opelopabt 4184* | Closed theorem form of opelopab 4193. (Contributed by NM, 19-Feb-2013.) |
⊢ ((∀𝑥∀𝑦(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥∀𝑦(𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | opelopabga 4185* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | brabga 4186* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) | ||
Theorem | opelopab2a 4187* | Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜓)) | ||
Theorem | opelopaba 4188* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | braba 4189* | The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜓) | ||
Theorem | opelopabg 4190* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | brabg 4191* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒)) | ||
Theorem | opelopab2 4192* | Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜒)) | ||
Theorem | opelopab 4193* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) | ||
Theorem | brab 4194* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜒) | ||
Theorem | opelopabaf 4195* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4193 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓) | ||
Theorem | opelopabf 4196* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4193 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜒 & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) | ||
Theorem | ssopab2 4197 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) | ||
Theorem | ssopab2b 4198 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
Theorem | ssopab2i 4199 | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} | ||
Theorem | ssopab2dv 4200* | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜒}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |