Home | Metamath
Proof Explorer Theorem List (p. 408 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pm10.57 40701 | Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥(𝜑 → (𝜓 ∨ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ∨ ∃𝑥(𝜑 ∧ 𝜒))) | ||
Theorem | 2alanimi 40702 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∀𝑥∀𝑦𝜒) | ||
Theorem | 2al2imi 40703 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒)) | ||
Theorem | pm11.11 40704 | Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑧∀𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 | ||
Theorem | pm11.12 40705* | Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥∀𝑦𝜓)) | ||
Theorem | 19.21vv 40706* | Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1936. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜓 → 𝜑) ↔ (𝜓 → ∀𝑥∀𝑦𝜑)) | ||
Theorem | 2alim 40707 | Theorem *11.32 in [WhiteheadRussell] p. 162. Theorem 19.20 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)) | ||
Theorem | 2albi 40708 | Theorem *11.33 in [WhiteheadRussell] p. 162. Theorem 19.15 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)) | ||
Theorem | 2exim 40709 | Theorem *11.34 in [WhiteheadRussell] p. 162. Theorem 19.22 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)) | ||
Theorem | 2exbi 40710 | Theorem *11.341 in [WhiteheadRussell] p. 162. Theorem 19.18 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)) | ||
Theorem | spsbce-2 40711 | Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑥∃𝑦𝜑) | ||
Theorem | 19.33-2 40712 | Theorem *11.421 in [WhiteheadRussell] p. 163. Theorem 19.33 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((∀𝑥∀𝑦𝜑 ∨ ∀𝑥∀𝑦𝜓) → ∀𝑥∀𝑦(𝜑 ∨ 𝜓)) | ||
Theorem | 19.36vv 40713* | Theorem *11.43 in [WhiteheadRussell] p. 163. Theorem 19.36 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 25-May-2011.) |
⊢ (∃𝑥∃𝑦(𝜑 → 𝜓) ↔ (∀𝑥∀𝑦𝜑 → 𝜓)) | ||
Theorem | 19.31vv 40714* | Theorem *11.44 in [WhiteheadRussell] p. 163. Theorem 19.31 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) ↔ (∀𝑥∀𝑦𝜑 ∨ 𝜓)) | ||
Theorem | 19.37vv 40715* | Theorem *11.46 in [WhiteheadRussell] p. 164. Theorem 19.37 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥∃𝑦(𝜓 → 𝜑) ↔ (𝜓 → ∃𝑥∃𝑦𝜑)) | ||
Theorem | 19.28vv 40716* | Theorem *11.47 in [WhiteheadRussell] p. 164. Theorem 19.28 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜓 ∧ 𝜑) ↔ (𝜓 ∧ ∀𝑥∀𝑦𝜑)) | ||
Theorem | pm11.52 40717 | Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥∀𝑦(𝜑 → ¬ 𝜓)) | ||
Theorem | aaanv 40718* | Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2349. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((∀𝑥𝜑 ∧ ∀𝑦𝜓) ↔ ∀𝑥∀𝑦(𝜑 ∧ 𝜓)) | ||
Theorem | pm11.57 40719* | Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑)) | ||
Theorem | pm11.58 40720* | Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑)) | ||
Theorem | pm11.59 40721* | Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑦∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜓 ∧ [𝑦 / 𝑥]𝜓))) | ||
Theorem | pm11.6 40722* | Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.) |
⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ∃𝑦(∃𝑥(𝜑 ∧ 𝜒) ∧ 𝜓)) | ||
Theorem | pm11.61 40723* | Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑦∀𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → ∃𝑦𝜓)) | ||
Theorem | pm11.62 40724* | Theorem *11.62 in [WhiteheadRussell] p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝜒) ↔ ∀𝑥(𝜑 → ∀𝑦(𝜓 → 𝜒))) | ||
Theorem | pm11.63 40725 | Theorem *11.63 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (¬ ∃𝑥∃𝑦𝜑 → ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
Theorem | pm11.7 40726 | Theorem *11.7 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜑) ↔ ∃𝑥∃𝑦𝜑) | ||
Theorem | pm11.71 40727* | Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑦(𝜒 → 𝜃)) ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃)))) | ||
Theorem | sbeqal1 40728* | If 𝑥 = 𝑦 always implies 𝑥 = 𝑧, then 𝑦 = 𝑧. (Contributed by Andrew Salmon, 2-Jun-2011.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧) → 𝑦 = 𝑧) | ||
Theorem | sbeqal1i 40729* | Suppose you know 𝑥 = 𝑦 implies 𝑥 = 𝑧, assuming 𝑥 and 𝑧 are distinct. Then, 𝑦 = 𝑧. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧) ⇒ ⊢ 𝑦 = 𝑧 | ||
Theorem | sbeqal2i 40730* | If 𝑥 = 𝑦 implies 𝑥 = 𝑧, then we can infer 𝑧 = 𝑦. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧) ⇒ ⊢ 𝑧 = 𝑦 | ||
Theorem | axc5c4c711 40731 | Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1792 as the inference rule. This proof extends the idea of axc5c711 36053 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.) |
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦(∀𝑦𝜑 → 𝜓) → (𝜑 → ∀𝑦(∀𝑦𝜑 → 𝜓))) → (∀𝑦𝜑 → ∀𝑦𝜓)) | ||
Theorem | axc5c4c711toc5 40732 | Rederivation of sp 2178 from axc5c4c711 40731. Note that ax6 2398 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1967 instead of ax6 2398, so that this rederivation requires only ax6v 1967 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c4c711toc4 40733 | Rederivation of axc4 2336 from axc5c4c711 40731. Note that only propositional calculus is required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | axc5c4c711toc7 40734 | Rederivation of axc7 2332 from axc5c4c711 40731. Note that neither axc7 2332 nor ax-11 2157 are required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c4c711to11 40735 | Rederivation of ax-11 2157 from axc5c4c711 40731. Note that ax-11 2157 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | axc11next 40736* | This theorem shows that, given axextb 2796, we can derive a version of axc11n 2444. However, it is weaker than axc11n 2444 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥) | ||
Theorem | pm13.13a 40737 | One result of theorem *13.13 in [WhiteheadRussell] p. 178. A note on the section - to make the theorems more usable, and because inequality is notation for set theory (it is not defined in the predicate calculus section), this section will use classes instead of sets. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑) | ||
Theorem | pm13.13b 40738 | Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ (([𝐴 / 𝑥]𝜑 ∧ 𝑥 = 𝐴) → 𝜑) | ||
Theorem | pm13.14 40739 | Theorem *13.14 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ (([𝐴 / 𝑥]𝜑 ∧ ¬ 𝜑) → 𝑥 ≠ 𝐴) | ||
Theorem | pm13.192 40740* | Theorem *13.192 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.) |
⊢ (∃𝑦(∀𝑥(𝑥 = 𝐴 ↔ 𝑥 = 𝑦) ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑) | ||
Theorem | pm13.193 40741 | Theorem *13.193 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝑥 = 𝑦)) | ||
Theorem | pm13.194 40742 | Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝜑 ∧ 𝑥 = 𝑦)) | ||
Theorem | pm13.195 40743* | Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3799. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.) |
⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑) | ||
Theorem | pm13.196a 40744* | Theorem *13.196 in [WhiteheadRussell] p. 179. The only difference is the position of the substituted variable. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ (¬ 𝜑 ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥)) | ||
Theorem | 2sbc6g 40745* | Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑧∀𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)) | ||
Theorem | 2sbc5g 40746* | Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)) | ||
Theorem | iotain 40747 | Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 15-Jul-2011.) |
⊢ (∃!𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} = (℩𝑥𝜑)) | ||
Theorem | iotaexeu 40748 | The iota class exists. This theorem does not require ax-nul 5209 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V) | ||
Theorem | iotasbc 40749* | Definition *14.01 in [WhiteheadRussell] p. 184. In Principia Mathematica, Russell and Whitehead define ℩ in terms of a function of (℩𝑥𝜑). Their definition differs in that a function of (℩𝑥𝜑) evaluates to "false" when there isn't a single 𝑥 that satisfies 𝜑. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝜓))) | ||
Theorem | iotasbc2 40750* | Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ ((∃!𝑥𝜑 ∧ ∃!𝑥𝜓) → ([(℩𝑥𝜑) / 𝑦][(℩𝑥𝜓) / 𝑧]𝜒 ↔ ∃𝑦∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∀𝑥(𝜓 ↔ 𝑥 = 𝑧) ∧ 𝜒))) | ||
Theorem | pm14.12 40751* | Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∃!𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | pm14.122a 40752* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑))) | ||
Theorem | pm14.122b 40753* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑))) | ||
Theorem | pm14.122c 40754* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑))) | ||
Theorem | pm14.123a 40755* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))) | ||
Theorem | pm14.123b 40756* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑))) | ||
Theorem | pm14.123c 40757* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑))) | ||
Theorem | pm14.18 40758 | Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∃!𝑥𝜑 → (∀𝑥𝜓 → [(℩𝑥𝜑) / 𝑥]𝜓)) | ||
Theorem | iotaequ 40759* | Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (℩𝑥𝑥 = 𝑦) = 𝑦 | ||
Theorem | iotavalb 40760* | Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 6328. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (℩𝑥𝜑) = 𝑦)) | ||
Theorem | iotasbc5 40761* | Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(𝑦 = (℩𝑥𝜑) ∧ 𝜓))) | ||
Theorem | pm14.24 40762* | Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑))) | ||
Theorem | iotavalsb 40763* | Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([𝑦 / 𝑧]𝜓 ↔ [(℩𝑥𝜑) / 𝑧]𝜓)) | ||
Theorem | sbiota1 40764 | Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) | ||
Theorem | sbaniota 40765 | Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) | ||
Theorem | eubiOLD 40766 | Obsolete proof of eubi 2665 as of 7-Oct-2022. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)) | ||
Theorem | iotasbcq 40767 | Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([(℩𝑥𝜑) / 𝑦]𝜒 ↔ [(℩𝑥𝜓) / 𝑦]𝜒)) | ||
Theorem | elnev 40768* | Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011.) |
⊢ (𝐴 ∈ V ↔ {𝑥 ∣ ¬ 𝑥 = 𝐴} ≠ V) | ||
Theorem | rusbcALT 40769 | A version of Russell's paradox which is proven using proper substitution. (Contributed by Andrew Salmon, 18-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V | ||
Theorem | compeq 40770* | Equality between two ways of saying "the complement of 𝐴". (Contributed by Andrew Salmon, 15-Jul-2011.) |
⊢ (V ∖ 𝐴) = {𝑥 ∣ ¬ 𝑥 ∈ 𝐴} | ||
Theorem | compne 40771 | The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.) |
⊢ (V ∖ 𝐴) ≠ 𝐴 | ||
Theorem | compab 40772 | Two ways of saying "the complement of a class abstraction". (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ (V ∖ {𝑧 ∣ 𝜑}) = {𝑧 ∣ ¬ 𝜑} | ||
Theorem | conss2 40773 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) |
⊢ (𝐴 ⊆ (V ∖ 𝐵) ↔ 𝐵 ⊆ (V ∖ 𝐴)) | ||
Theorem | conss1 40774 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) |
⊢ ((V ∖ 𝐴) ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ 𝐴) | ||
Theorem | ralbidar 40775 | More general form of ralbida 3230. (Contributed by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidar 40776 | More general form of rexbida 3318. (Contributed by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | dropab1 40777 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) |
⊢ (∀𝑥 𝑥 = 𝑦 → {〈𝑥, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ 𝜑}) | ||
Theorem | dropab2 40778 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) |
⊢ (∀𝑥 𝑥 = 𝑦 → {〈𝑧, 𝑥〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜑}) | ||
Theorem | ipo0 40779 | If the identity relation partially orders any class, then that class is the null class. (Contributed by Andrew Salmon, 25-Jul-2011.) |
⊢ ( I Po 𝐴 ↔ 𝐴 = ∅) | ||
Theorem | ifr0 40780 | A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.) |
⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅) | ||
Theorem | ordpss 40781 | ordelpss 6218 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.) |
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵)) | ||
Theorem | fvsb 40782* | Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (∃!𝑦 𝐴𝐹𝑦 → ([(𝐹‘𝐴) / 𝑥]𝜑 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑))) | ||
Theorem | fveqsb 40783* | Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (𝑥 = (𝐹‘𝐴) → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃!𝑦 𝐴𝐹𝑦 → (𝜓 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑))) | ||
Theorem | xpexb 40784 | A Cartesian product exists iff its converse does. Corollary 6.9(1) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.) |
⊢ ((𝐴 × 𝐵) ∈ V ↔ (𝐵 × 𝐴) ∈ V) | ||
Theorem | trelpss 40785 | An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5538, ax-reg 9055 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.) |
⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊊ 𝐴) | ||
Theorem | addcomgi 40786 | Generalization of commutative law for addition. Simplifies proofs dealing with vectors. However, it is dependent on our particular definition of ordered pair. (Contributed by Andrew Salmon, 28-Jan-2012.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) | ||
Syntax | cplusr 40787 | Introduce the operation of vector addition. |
class +𝑟 | ||
Syntax | cminusr 40788 | Introduce the operation of vector subtraction. |
class -𝑟 | ||
Syntax | ctimesr 40789 | Introduce the operation of scalar multiplication. |
class .𝑣 | ||
Syntax | cptdfc 40790 | PtDf is a predicate that is crucial for the definition of lines as well as proving a number of important theorems. |
class PtDf(𝐴, 𝐵) | ||
Syntax | crr3c 40791 | RR3 is a class. |
class RR3 | ||
Syntax | cline3 40792 | line3 is a class. |
class line3 | ||
Definition | df-addr 40793* | Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) |
⊢ +𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) + (𝑦‘𝑣)))) | ||
Definition | df-subr 40794* | Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) |
⊢ -𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣)))) | ||
Definition | df-mulv 40795* | Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) |
⊢ .𝑣 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ (𝑥 · (𝑦‘𝑣)))) | ||
Theorem | addrval 40796* | Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) + (𝐵‘𝑣)))) | ||
Theorem | subrval 40797* | Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) − (𝐵‘𝑣)))) | ||
Theorem | mulvval 40798* | Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) = (𝑣 ∈ ℝ ↦ (𝐴 · (𝐵‘𝑣)))) | ||
Theorem | addrfv 40799 | Vector addition at a value. The operation takes each vector 𝐴 and 𝐵 and forms a new vector whose values are the sum of each of the values of 𝐴 and 𝐵. (Contributed by Andrew Salmon, 27-Jan-2012.) |
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴+𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) + (𝐵‘𝐶))) | ||
Theorem | subrfv 40800 | Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.) |
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴-𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) − (𝐵‘𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |