| Metamath
Proof Explorer Theorem List (p. 445 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 19.33-2 44401 | 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 44402* | 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 44403* | 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 44404* | 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 44405* | 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 44406 | Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
| ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥∀𝑦(𝜑 → ¬ 𝜓)) | ||
| Theorem | aaanv 44407* | Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2333. (Contributed by Andrew Salmon, 24-May-2011.) |
| ⊢ ((∀𝑥𝜑 ∧ ∀𝑦𝜓) ↔ ∀𝑥∀𝑦(𝜑 ∧ 𝜓)) | ||
| Theorem | pm11.57 44408* | Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.) |
| ⊢ (∀𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑)) | ||
| Theorem | pm11.58 44409* | Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.) |
| ⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑)) | ||
| Theorem | pm11.59 44410* | Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.) |
| ⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑦∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜓 ∧ [𝑦 / 𝑥]𝜓))) | ||
| Theorem | pm11.6 44411* | Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.) |
| ⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ∃𝑦(∃𝑥(𝜑 ∧ 𝜒) ∧ 𝜓)) | ||
| Theorem | pm11.61 44412* | Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
| ⊢ (∃𝑦∀𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → ∃𝑦𝜓)) | ||
| Theorem | pm11.62 44413* | Theorem *11.62 in [WhiteheadRussell] p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
| ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝜒) ↔ ∀𝑥(𝜑 → ∀𝑦(𝜓 → 𝜒))) | ||
| Theorem | pm11.63 44414 | Theorem *11.63 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
| ⊢ (¬ ∃𝑥∃𝑦𝜑 → ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
| Theorem | pm11.7 44415 | Theorem *11.7 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
| ⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜑) ↔ ∃𝑥∃𝑦𝜑) | ||
| Theorem | pm11.71 44416* | Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.) |
| ⊢ ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑦(𝜒 → 𝜃)) ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃)))) | ||
| Theorem | sbeqal1 44417* | If 𝑥 = 𝑦 always implies 𝑥 = 𝑧, then 𝑦 = 𝑧. (Contributed by Andrew Salmon, 2-Jun-2011.) |
| ⊢ (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧) → 𝑦 = 𝑧) | ||
| Theorem | sbeqal1i 44418* | Suppose you know 𝑥 = 𝑦 implies 𝑥 = 𝑧, assuming 𝑥 and 𝑧 are distinct. Then, 𝑦 = 𝑧. (Contributed by Andrew Salmon, 3-Jun-2011.) |
| ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧) ⇒ ⊢ 𝑦 = 𝑧 | ||
| Theorem | sbeqal2i 44419* | If 𝑥 = 𝑦 implies 𝑥 = 𝑧, then we can infer 𝑧 = 𝑦. (Contributed by Andrew Salmon, 3-Jun-2011.) |
| ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧) ⇒ ⊢ 𝑧 = 𝑦 | ||
| Theorem | axc5c4c711 44420 | Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1795 as the inference rule. This proof extends the idea of axc5c711 38919 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.) |
| ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦(∀𝑦𝜑 → 𝜓) → (𝜑 → ∀𝑦(∀𝑦𝜑 → 𝜓))) → (∀𝑦𝜑 → ∀𝑦𝜓)) | ||
| Theorem | axc5c4c711toc5 44421 | Rederivation of sp 2183 from axc5c4c711 44420. Note that ax6 2389 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1968 instead of ax6 2389, so that this rederivation requires only ax6v 1968 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → 𝜑) | ||
| Theorem | axc5c4c711toc4 44422 | Rederivation of axc4 2321 from axc5c4c711 44420. 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 44423 | Rederivation of axc7 2317 from axc5c4c711 44420. Note that neither axc7 2317 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 44424 | Rederivation of ax-11 2157 from axc5c4c711 44420. 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 44425* | This theorem shows that, given axextb 2711, we can derive a version of axc11n 2431. However, it is weaker than axc11n 2431 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 44426 | 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 44427 | Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.) |
| ⊢ (([𝐴 / 𝑥]𝜑 ∧ 𝑥 = 𝐴) → 𝜑) | ||
| Theorem | pm13.14 44428 | Theorem *13.14 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) |
| ⊢ (([𝐴 / 𝑥]𝜑 ∧ ¬ 𝜑) → 𝑥 ≠ 𝐴) | ||
| Theorem | pm13.192 44429* | Theorem *13.192 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.) |
| ⊢ (∃𝑦(∀𝑥(𝑥 = 𝐴 ↔ 𝑥 = 𝑦) ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑) | ||
| Theorem | pm13.193 44430 | Theorem *13.193 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝑥 = 𝑦)) | ||
| Theorem | pm13.194 44431 | Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝜑 ∧ 𝑥 = 𝑦)) | ||
| Theorem | pm13.195 44432* | Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3816. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.) |
| ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑) | ||
| Theorem | pm13.196a 44433* | 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 44434* | Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑧∀𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)) | ||
| Theorem | 2sbc5g 44435* | Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)) | ||
| Theorem | iotain 44436 | Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 15-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} = (℩𝑥𝜑)) | ||
| Theorem | iotaexeu 44437 | The iota class exists. This theorem does not require ax-nul 5306 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V) | ||
| Theorem | iotasbc 44438* | 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 44439* | Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ ((∃!𝑥𝜑 ∧ ∃!𝑥𝜓) → ([(℩𝑥𝜑) / 𝑦][(℩𝑥𝜓) / 𝑧]𝜒 ↔ ∃𝑦∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∀𝑥(𝜓 ↔ 𝑥 = 𝑧) ∧ 𝜒))) | ||
| Theorem | pm14.12 44440* | Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
| Theorem | pm14.122a 44441* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
| ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑))) | ||
| Theorem | pm14.122b 44442* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
| ⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑))) | ||
| Theorem | pm14.122c 44443* | Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
| ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑))) | ||
| Theorem | pm14.123a 44444* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))) | ||
| Theorem | pm14.123b 44445* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑))) | ||
| Theorem | pm14.123c 44446* | Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑))) | ||
| Theorem | pm14.18 44447 | Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → (∀𝑥𝜓 → [(℩𝑥𝜑) / 𝑥]𝜓)) | ||
| Theorem | iotaequ 44448* | Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (℩𝑥𝑥 = 𝑦) = 𝑦 | ||
| Theorem | iotavalb 44449* | Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 6532. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (℩𝑥𝜑) = 𝑦)) | ||
| Theorem | iotasbc5 44450* | Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(𝑦 = (℩𝑥𝜑) ∧ 𝜓))) | ||
| Theorem | pm14.24 44451* | Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑))) | ||
| Theorem | iotavalsb 44452* | Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([𝑦 / 𝑧]𝜓 ↔ [(℩𝑥𝜑) / 𝑧]𝜓)) | ||
| Theorem | sbiota1 44453 | Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) | ||
| Theorem | sbaniota 44454 | Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.) |
| ⊢ (∃!𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) | ||
| Theorem | eubiOLD 44455 | Obsolete proof of eubi 2584 as of 7-Oct-2022. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)) | ||
| Theorem | iotasbcq 44456 | Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| ⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([(℩𝑥𝜑) / 𝑦]𝜒 ↔ [(℩𝑥𝜓) / 𝑦]𝜒)) | ||
| Theorem | elnev 44457* | 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 44458 | 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 44459* | Equality between two ways of saying "the complement of 𝐴". (Contributed by Andrew Salmon, 15-Jul-2011.) |
| ⊢ (V ∖ 𝐴) = {𝑥 ∣ ¬ 𝑥 ∈ 𝐴} | ||
| Theorem | compne 44460 | The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.) |
| ⊢ (V ∖ 𝐴) ≠ 𝐴 | ||
| Theorem | compab 44461 | 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 44462 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) |
| ⊢ (𝐴 ⊆ (V ∖ 𝐵) ↔ 𝐵 ⊆ (V ∖ 𝐴)) | ||
| Theorem | conss1 44463 | Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.) |
| ⊢ ((V ∖ 𝐴) ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ 𝐴) | ||
| Theorem | ralbidar 44464 | More general form of ralbida 3270. (Contributed by Andrew Salmon, 25-Jul-2011.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
| Theorem | rexbidar 44465 | More general form of rexbida 3272. (Contributed by Andrew Salmon, 25-Jul-2011.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
| Theorem | dropab1 44466 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → {〈𝑥, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ 𝜑}) | ||
| Theorem | dropab2 44467 | Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → {〈𝑧, 𝑥〉 ∣ 𝜑} = {〈𝑧, 𝑦〉 ∣ 𝜑}) | ||
| Theorem | ipo0 44468 | 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 44469 | A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.) |
| ⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅) | ||
| Theorem | ordpss 44470 | ordelpss 6412 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.) |
| ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵)) | ||
| Theorem | fvsb 44471* | Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) |
| ⊢ (∃!𝑦 𝐴𝐹𝑦 → ([(𝐹‘𝐴) / 𝑥]𝜑 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑))) | ||
| Theorem | fveqsb 44472* | Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.) |
| ⊢ (𝑥 = (𝐹‘𝐴) → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃!𝑦 𝐴𝐹𝑦 → (𝜓 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑))) | ||
| Theorem | xpexb 44473 | 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 44474 | An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5668, ax-reg 9632 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.) |
| ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊊ 𝐴) | ||
| Theorem | addcomgi 44475 | 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 44476 | Introduce the operation of vector addition. |
| class +𝑟 | ||
| Syntax | cminusr 44477 | Introduce the operation of vector subtraction. |
| class -𝑟 | ||
| Syntax | ctimesr 44478 | Introduce the operation of scalar multiplication. |
| class .𝑣 | ||
| Syntax | cptdfc 44479 | 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 44480 | RR3 is a class. |
| class RR3 | ||
| Syntax | cline3 44481 | line3 is a class. |
| class line3 | ||
| Definition | df-addr 44482* | Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ +𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) + (𝑦‘𝑣)))) | ||
| Definition | df-subr 44483* | Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ -𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣)))) | ||
| Definition | df-mulv 44484* | Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ .𝑣 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ (𝑥 · (𝑦‘𝑣)))) | ||
| Theorem | addrval 44485* | Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) + (𝐵‘𝑣)))) | ||
| Theorem | subrval 44486* | Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) − (𝐵‘𝑣)))) | ||
| Theorem | mulvval 44487* | Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) = (𝑣 ∈ ℝ ↦ (𝐴 · (𝐵‘𝑣)))) | ||
| Theorem | addrfv 44488 | 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 44489 | Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴-𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) − (𝐵‘𝐶))) | ||
| Theorem | mulvfv 44490 | Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴.𝑣𝐵)‘𝐶) = (𝐴 · (𝐵‘𝐶))) | ||
| Theorem | addrfn 44491 | Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) Fn ℝ) | ||
| Theorem | subrfn 44492 | Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) Fn ℝ) | ||
| Theorem | mulvfn 44493 | Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) Fn ℝ) | ||
| Theorem | addrcom 44494 | Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝐵+𝑟𝐴)) | ||
| Definition | df-ptdf 44495* | Define the predicate PtDf, which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) |
| ⊢ PtDf(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3})) | ||
| Definition | df-rr3 44496 | Define the set of all points RR3. We define each point 𝐴 as a function to allow the use of vector addition and subtraction as well as scalar multiplication in our proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) |
| ⊢ RR3 = (ℝ ↑m {1, 2, 3}) | ||
| Definition | df-line3 44497* | Define the set of all lines. A line is an infinite subset of RR3 that satisfies a PtDf property. (Contributed by Andrew Salmon, 15-Jul-2012.) |
| ⊢ line3 = {𝑥 ∈ 𝒫 RR3 ∣ (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))} | ||
We are sad to report the passing of long-time contributor Alan Sare (Nov. 9, 1954 - Mar. 23, 2019). Alan's first contribution to Metamath was a shorter proof for tfrlem8 8424 in 2008. He developed a tool called "completeusersproof" that assists developing proofs using his "virtual deduction" method: https://us.metamath.org/other.html#completeusersproof 8424. His virtual deduction method is explained in the comment for wvd1 44589. Below are some excerpts from his first emails to NM in 2007: ...I have been interested in proving set theory theorems for many years for mental exercise. I enjoy it. I have used a book by Martin Zuckerman. It is informal. I am interested in completely and perfectly proving theorems. Mr. Zuckerman leaves out most of the steps of a proof, of course, like most authors do, as you have noted. A complete proof for higher theorems would require a volume of writing similar to the Metamath documents. So I am frustrated when I am not capable of constructing a proof and Zuckerman leaves out steps I do not understand. I could search for the steps in other texts, but I don't do that too much. Metamath may be the answer for me.... ...If we go beyond mathematics, I believe that it is possible to write down all human knowledge in a way similar to the way you have explicated large areas of mathematics. Of course, that would be a much, much more difficult job. For example, it is possible to take a hard science like physics, construct axioms based on experimental results, and to cast all of physics into a collection of axioms and theorems. Maybe this has already been attempted, although I am not familiar with it. When one then moves on to the soft sciences such as social science, this job gets much more difficult. The key is: All human thought consists of logical operations on abstract objects. Usually, these logical operations are done informally. There is no reason why one cannot take any subject and explicate it and take it down to the indivisible postulates in a formal rigorous way.... ...When I read a math book or an engineering book I come across something I don't understand and I am compelled to understand it. But, often it is hopeless. I don't have the time. Or, I would have to read the same thing by multiple authors in the hope that different authors would give parts of the working proof that others have omitted. It is very inefficient. Because I have always been inclined to "get to the bottom" for a 100% fully understood proof.... | ||
| Theorem | idiALT 44498 | Placeholder for idi 1. Though unnecessary, this theorem is sometimes used in proofs in this mathbox for pedagogical purposes. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 ⇒ ⊢ 𝜑 | ||
| Theorem | exbir 44499 | Exportation implication also converting the consequent from a biconditional to an implication. Derived automatically from exbirVD 44873. (Contributed by Alan Sare, 31-Dec-2011.) |
| ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) | ||
| Theorem | 3impexpbicom 44500 | Version of 3impexp 1359 where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |