Home Metamath Proof ExplorerTheorem List (p. 377 of 424) < 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-27159) Hilbert Space Explorer (27160-28684) Users' Mathboxes (28685-42360)

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theorem2exbi 37601 Theorem *11.341 in [WhiteheadRussell] p. 162. Theorem 19.18 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
(∀𝑥𝑦(𝜑𝜓) → (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓))

Theoremspsbce-2 37602 Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.)
([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑥𝑦𝜑)

Theorem19.33-2 37603 Theorem *11.421 in [WhiteheadRussell] p. 163. Theorem 19.33 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
((∀𝑥𝑦𝜑 ∨ ∀𝑥𝑦𝜓) → ∀𝑥𝑦(𝜑𝜓))

Theorem19.36vv 37604* Theorem *11.43 in [WhiteheadRussell] p. 163. Theorem 19.36 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 25-May-2011.)
(∃𝑥𝑦(𝜑𝜓) ↔ (∀𝑥𝑦𝜑𝜓))

Theorem19.31vv 37605* Theorem *11.44 in [WhiteheadRussell] p. 163. Theorem 19.31 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
(∀𝑥𝑦(𝜑𝜓) ↔ (∀𝑥𝑦𝜑𝜓))

Theorem19.37vv 37606* Theorem *11.46 in [WhiteheadRussell] p. 164. Theorem 19.37 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
(∃𝑥𝑦(𝜓𝜑) ↔ (𝜓 → ∃𝑥𝑦𝜑))

Theorem19.28vv 37607* Theorem *11.47 in [WhiteheadRussell] p. 164. Theorem 19.28 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
(∀𝑥𝑦(𝜓𝜑) ↔ (𝜓 ∧ ∀𝑥𝑦𝜑))

Theorempm11.52 37608 Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
(∃𝑥𝑦(𝜑𝜓) ↔ ¬ ∀𝑥𝑦(𝜑 → ¬ 𝜓))

Theorem2exanali 37609 Theorem *11.521 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
(¬ ∃𝑥𝑦(𝜑 ∧ ¬ 𝜓) ↔ ∀𝑥𝑦(𝜑𝜓))

Theoremaaanv 37610* Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2156. (Contributed by Andrew Salmon, 24-May-2011.)
((∀𝑥𝜑 ∧ ∀𝑦𝜓) ↔ ∀𝑥𝑦(𝜑𝜓))

Theorempm11.57 37611* Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
(∀𝑥𝜑 ↔ ∀𝑥𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))

Theorempm11.58 37612* Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
(∃𝑥𝜑 ↔ ∃𝑥𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))

Theorempm11.59 37613* Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
(∀𝑥(𝜑𝜓) → ∀𝑦𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜓 ∧ [𝑦 / 𝑥]𝜓)))

Theorempm11.6 37614* Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
(∃𝑥(∃𝑦(𝜑𝜓) ∧ 𝜒) ↔ ∃𝑦(∃𝑥(𝜑𝜒) ∧ 𝜓))

Theorempm11.61 37615* Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
(∃𝑦𝑥(𝜑𝜓) → ∀𝑥(𝜑 → ∃𝑦𝜓))

Theorempm11.62 37616* Theorem *11.62 in [WhiteheadRussell] p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
(∀𝑥𝑦((𝜑𝜓) → 𝜒) ↔ ∀𝑥(𝜑 → ∀𝑦(𝜓𝜒)))

Theorempm11.63 37617 Theorem *11.63 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
(¬ ∃𝑥𝑦𝜑 → ∀𝑥𝑦(𝜑𝜓))

Theorempm11.7 37618 Theorem *11.7 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
(∃𝑥𝑦(𝜑𝜑) ↔ ∃𝑥𝑦𝜑)

Theorempm11.71 37619* Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃)) ↔ ∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃))))

21.29.3  Predicate Calculus

Theoremsbeqal1 37620* If 𝑥 = 𝑦 always implies 𝑥 = 𝑧, then 𝑦 = 𝑧 is true. (Contributed by Andrew Salmon, 2-Jun-2011.)
(∀𝑥(𝑥 = 𝑦𝑥 = 𝑧) → 𝑦 = 𝑧)

Theoremsbeqal1i 37621* Suppose you know 𝑥 = 𝑦 implies 𝑥 = 𝑧, assuming 𝑥 and 𝑧 are distinct. Then, 𝑦 = 𝑧. (Contributed by Andrew Salmon, 3-Jun-2011.)
(𝑥 = 𝑦𝑥 = 𝑧)       𝑦 = 𝑧

Theoremsbeqal2i 37622* If 𝑥 = 𝑦 implies 𝑥 = 𝑧, then we can infer 𝑧 = 𝑦. (Contributed by Andrew Salmon, 3-Jun-2011.)
(𝑥 = 𝑦𝑥 = 𝑧)       𝑧 = 𝑦

Theoremsbeqalbi 37623* When both 𝑥 and 𝑧 and 𝑦 and 𝑧 are both distinct, then the converse of sbeqal1 holds as well. (Contributed by Andrew Salmon, 2-Jun-2011.)
(𝑥 = 𝑦 ↔ ∀𝑧(𝑧 = 𝑥𝑧 = 𝑦))

Theoremaxc5c4c711 37624 Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1713 as the inference rule. This proof extends the idea of axc5c711 33221 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.)
((∀𝑥𝑦 ¬ ∀𝑥𝑦(∀𝑦𝜑𝜓) → (𝜑 → ∀𝑦(∀𝑦𝜑𝜓))) → (∀𝑦𝜑 → ∀𝑦𝜓))

Theoremaxc5c4c711toc5 37625 Rederivation of sp 2041 from axc5c4c711 37624. Note that ax6 2239 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1876 instead of ax6 2239, so that this rederivation requires only ax6v 1876 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
(∀𝑥𝜑𝜑)

Theoremaxc5c4c711toc4 37626 Rederivation of axc4 2115 from axc5c4c711 37624. 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.)
(∀𝑥(∀𝑥𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))

Theoremaxc5c4c711toc7 37627 Rederivation of axc7 2117 from axc5c4c711 37624. Note that neither axc7 2117 nor ax-11 2021 are required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(¬ ∀𝑥 ¬ ∀𝑥𝜑𝜑)

Theoremaxc5c4c711to11 37628 Rederivation of ax-11 2021 from axc5c4c711 37624. Note that ax-11 2021 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)

Theoremaxc11next 37629* This theorem shows that, given axext4 2594, we can derive a version of axc11n 2295. However, it is weaker than axc11n 2295 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)

21.29.4  Principia Mathematica * 13 and * 14

Theorempm13.13a 37630 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.)
((𝜑𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑)

Theorempm13.13b 37631 Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.)
(([𝐴 / 𝑥]𝜑𝑥 = 𝐴) → 𝜑)

Theorempm13.14 37632 Theorem *13.14 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
(([𝐴 / 𝑥]𝜑 ∧ ¬ 𝜑) → 𝑥𝐴)

Theorempm13.192 37633* Theorem *13.192 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
(∃𝑦(∀𝑥(𝑥 = 𝐴𝑥 = 𝑦) ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑)

Theorempm13.193 37634 Theorem *13.193 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
((𝜑𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑𝑥 = 𝑦))

Theorempm13.194 37635 Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
((𝜑𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑𝜑𝑥 = 𝑦))

Theorempm13.195 37636* Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3427. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
(∃𝑦(𝑦 = 𝐴𝜑) ↔ [𝐴 / 𝑦]𝜑)

Theorempm13.196a 37637* Theorem *13.196 in [WhiteheadRussell] p. 179. The only difference is the position of the substituted variable. (Contributed by Andrew Salmon, 3-Jun-2011.)
𝜑 ↔ ∀𝑦([𝑦 / 𝑥]𝜑𝑦𝑥))

Theorem2sbc6g 37638* Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
((𝐴𝐶𝐵𝐷) → (∀𝑧𝑤((𝑧 = 𝐴𝑤 = 𝐵) → 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))

Theorem2sbc5g 37639* Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
((𝐴𝐶𝐵𝐷) → (∃𝑧𝑤((𝑧 = 𝐴𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))

Theoremiotain 37640 Equivalence between two different forms of . (Contributed by Andrew Salmon, 15-Jul-2011.)
(∃!𝑥𝜑 {𝑥𝜑} = (℩𝑥𝜑))

Theoremiotaexeu 37641 The iota class exists. This theorem does not require ax-nul 4717 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.)
(∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)

Theoremiotasbc 37642* 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.)
(∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(∀𝑥(𝜑𝑥 = 𝑦) ∧ 𝜓)))

Theoremiotasbc2 37643* Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
((∃!𝑥𝜑 ∧ ∃!𝑥𝜓) → ([(℩𝑥𝜑) / 𝑦][(℩𝑥𝜓) / 𝑧]𝜒 ↔ ∃𝑦𝑧(∀𝑥(𝜑𝑥 = 𝑦) ∧ ∀𝑥(𝜓𝑥 = 𝑧) ∧ 𝜒)))

Theorempm14.12 37644* Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
(∃!𝑥𝜑 → ∀𝑥𝑦((𝜑[𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))

Theorempm14.122a 37645* Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
(𝐴𝑉 → (∀𝑥(𝜑𝑥 = 𝐴) ↔ (∀𝑥(𝜑𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑)))

Theorempm14.122b 37646* Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
(𝐴𝑉 → ((∀𝑥(𝜑𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑) ↔ (∀𝑥(𝜑𝑥 = 𝐴) ∧ ∃𝑥𝜑)))

Theorempm14.122c 37647* Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
(𝐴𝑉 → (∀𝑥(𝜑𝑥 = 𝐴) ↔ (∀𝑥(𝜑𝑥 = 𝐴) ∧ ∃𝑥𝜑)))

Theorempm14.123a 37648* Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
((𝐴𝑉𝐵𝑊) → (∀𝑧𝑤(𝜑 ↔ (𝑧 = 𝐴𝑤 = 𝐵)) ↔ (∀𝑧𝑤(𝜑 → (𝑧 = 𝐴𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)))

Theorempm14.123b 37649* Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
((𝐴𝑉𝐵𝑊) → ((∀𝑧𝑤(𝜑 → (𝑧 = 𝐴𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∀𝑧𝑤(𝜑 → (𝑧 = 𝐴𝑤 = 𝐵)) ∧ ∃𝑧𝑤𝜑)))

Theorempm14.123c 37650* Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
((𝐴𝑉𝐵𝑊) → (∀𝑧𝑤(𝜑 ↔ (𝑧 = 𝐴𝑤 = 𝐵)) ↔ (∀𝑧𝑤(𝜑 → (𝑧 = 𝐴𝑤 = 𝐵)) ∧ ∃𝑧𝑤𝜑)))

Theorempm14.18 37651 Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
(∃!𝑥𝜑 → (∀𝑥𝜓[(℩𝑥𝜑) / 𝑥]𝜓))

Theoremiotaequ 37652* Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
(℩𝑥𝑥 = 𝑦) = 𝑦

Theoremiotavalb 37653* Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 5779. (Contributed by Andrew Salmon, 11-Jul-2011.)
(∃!𝑥𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) ↔ (℩𝑥𝜑) = 𝑦))

Theoremiotasbc5 37654* Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.)
(∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(𝑦 = (℩𝑥𝜑) ∧ 𝜓)))

Theorempm14.24 37655* Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
(∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑𝑦 = (℩𝑥𝜑)))

Theoremiotavalsb 37656* Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
(∀𝑥(𝜑𝑥 = 𝑦) → ([𝑦 / 𝑧]𝜓[(℩𝑥𝜑) / 𝑧]𝜓))

Theoremsbiota1 37657 Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
(∃!𝑥𝜑 → (∀𝑥(𝜑𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))

Theoremsbaniota 37658 Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
(∃!𝑥𝜑 → (∃𝑥(𝜑𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))

Theoremeubi 37659 Theorem *14.271 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
(∀𝑥(𝜑𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))

Theoremiotasbcq 37660 Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.)
(∀𝑥(𝜑𝜓) → ([(℩𝑥𝜑) / 𝑦]𝜒[(℩𝑥𝜓) / 𝑦]𝜒))

21.29.5  Set Theory

Theoremelnev 37661* Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011.)
(𝐴 ∈ V ↔ {𝑥 ∣ ¬ 𝑥 = 𝐴} ≠ V)

TheoremrusbcALT 37662 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

Theoremcompel 37663 Equivalence between two ways of saying "is a member of the complement of 𝐴." (Contributed by Andrew Salmon, 15-Jul-2011.)
(𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥𝐴)

Theoremcompeq 37664* Equality between two ways of saying "the complement of 𝐴." (Contributed by Andrew Salmon, 15-Jul-2011.)
(V ∖ 𝐴) = {𝑥 ∣ ¬ 𝑥𝐴}

Theoremcompne 37665 The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.)
(V ∖ 𝐴) ≠ 𝐴

Theoremcompab 37666 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 ∖ {𝑧𝜑}) = {𝑧 ∣ ¬ 𝜑}

Theoremconss34OLD 37667 Obsolete proof of complss 3713 as of 7-Aug-2021. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴))

Theoremconss2 37668 Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
(𝐴 ⊆ (V ∖ 𝐵) ↔ 𝐵 ⊆ (V ∖ 𝐴))

Theoremconss1 37669 Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
((V ∖ 𝐴) ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ 𝐴)

Theoremralbidar 37670 More general form of ralbida 2965. (Contributed by Andrew Salmon, 25-Jul-2011.)
(𝜑 → ∀𝑥𝐴 𝜑)    &   ((𝜑𝑥𝐴) → (𝜓𝜒))       (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))

Theoremrexbidar 37671 More general form of rexbida 3029. (Contributed by Andrew Salmon, 25-Jul-2011.)
(𝜑 → ∀𝑥𝐴 𝜑)    &   ((𝜑𝑥𝐴) → (𝜓𝜒))       (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))

Theoremdropab1 37672 Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
(∀𝑥 𝑥 = 𝑦 → {⟨𝑥, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ 𝜑})

Theoremdropab2 37673 Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
(∀𝑥 𝑥 = 𝑦 → {⟨𝑧, 𝑥⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜑})

Theoremipo0 37674 If the identity relation partially orders any class, then that class is the null class. (Contributed by Andrew Salmon, 25-Jul-2011.)
( I Po 𝐴𝐴 = ∅)

Theoremifr0 37675 A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.)
( I Fr 𝐴𝐴 = ∅)

Theoremordpss 37676 ordelpss 5668 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.)
(Ord 𝐵 → (𝐴𝐵𝐴𝐵))

Theoremfvsb 37677* Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
(∃!𝑦 𝐴𝐹𝑦 → ([(𝐹𝐴) / 𝑥]𝜑 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦𝑦 = 𝑥) ∧ 𝜑)))

Theoremfveqsb 37678* Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
(𝑥 = (𝐹𝐴) → (𝜑𝜓))    &   𝑥𝜓       (∃!𝑦 𝐴𝐹𝑦 → (𝜓 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦𝑦 = 𝑥) ∧ 𝜑)))

Theoremxpexb 37679 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)

Theoremtrelpss 37680 An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5022, ax-reg 8380 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.)
((Tr 𝐴𝐵𝐴) → 𝐵𝐴)

21.29.6  Arithmetic

Theoremaddcomgi 37681 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.)
(𝐴 + 𝐵) = (𝐵 + 𝐴)

21.29.7  Geometry

Syntaxcplusr 37682 Introduce the operation of vector addition.
class +𝑟

Syntaxcminusr 37683 Introduce the operation of vector subtraction.
class -𝑟

Syntaxctimesr 37684 Introduce the operation of scalar multiplication.
class .𝑣

Syntaxcptdfc 37685 PtDf is a predicate that is crucial for the definition of lines as well as proving a number of important theorems.
class PtDf(𝐴, 𝐵)

Syntaxcrr3c 37686 RR3 is a class.
class RR3

Syntaxcline3 37687 line3 is a class.
class line3

Definitiondf-addr 37688* Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)
+𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥𝑣) + (𝑦𝑣))))

Definitiondf-subr 37689* Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)
-𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥𝑣) − (𝑦𝑣))))

Definitiondf-mulv 37690* Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)
.𝑣 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ (𝑥 · (𝑦𝑣))))

Theoremaddrval 37691* Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)
((𝐴𝐶𝐵𝐷) → (𝐴+𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴𝑣) + (𝐵𝑣))))

Theoremsubrval 37692* Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)
((𝐴𝐶𝐵𝐷) → (𝐴-𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴𝑣) − (𝐵𝑣))))

Theoremmulvval 37693* Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)
((𝐴𝐶𝐵𝐷) → (𝐴.𝑣𝐵) = (𝑣 ∈ ℝ ↦ (𝐴 · (𝐵𝑣))))

Theoremaddrfv 37694 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.)
((𝐴𝐸𝐵𝐷𝐶 ∈ ℝ) → ((𝐴+𝑟𝐵)‘𝐶) = ((𝐴𝐶) + (𝐵𝐶)))

Theoremsubrfv 37695 Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)
((𝐴𝐸𝐵𝐷𝐶 ∈ ℝ) → ((𝐴-𝑟𝐵)‘𝐶) = ((𝐴𝐶) − (𝐵𝐶)))

Theoremmulvfv 37696 Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)
((𝐴𝐸𝐵𝐷𝐶 ∈ ℝ) → ((𝐴.𝑣𝐵)‘𝐶) = (𝐴 · (𝐵𝐶)))

Theoremaddrfn 37697 Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
((𝐴𝐶𝐵𝐷) → (𝐴+𝑟𝐵) Fn ℝ)

Theoremsubrfn 37698 Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
((𝐴𝐶𝐵𝐷) → (𝐴-𝑟𝐵) Fn ℝ)

Theoremmulvfn 37699 Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
((𝐴𝐶𝐵𝐷) → (𝐴.𝑣𝐵) Fn ℝ)