Home Metamath Proof ExplorerTheorem List (p. 385 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-27745) Hilbert Space Explorer (27746-29270) Users' Mathboxes (29271-42316)

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

Theorem19.33-2 38401 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 38402* 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 38403* 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 38404* 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 38405* 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 38406 Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
(∃𝑥𝑦(𝜑𝜓) ↔ ¬ ∀𝑥𝑦(𝜑 → ¬ 𝜓))

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

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

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

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

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

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

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

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

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

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

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

20.29.3  Predicate Calculus

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

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

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

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

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

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

Theoremaxc5c4c711toc4 38424 Rederivation of axc4 2128 from axc5c4c711 38422. 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 38425 Rederivation of axc7 2130 from axc5c4c711 38422. Note that neither axc7 2130 nor ax-11 2032 are required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(¬ ∀𝑥 ¬ ∀𝑥𝜑𝜑)

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

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

20.29.4  Principia Mathematica * 13 and * 14

Theorempm13.13a 38428 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 38429 Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.)
(([𝐴 / 𝑥]𝜑𝑥 = 𝐴) → 𝜑)

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

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

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

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

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

Theorempm13.196a 38435* 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 38436* Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
((𝐴𝐶𝐵𝐷) → (∀𝑧𝑤((𝑧 = 𝐴𝑤 = 𝐵) → 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))

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

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

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

Theoremiotasbc 38440* 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 38441* Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
((∃!𝑥𝜑 ∧ ∃!𝑥𝜓) → ([(℩𝑥𝜑) / 𝑦][(℩𝑥𝜓) / 𝑧]𝜒 ↔ ∃𝑦𝑧(∀𝑥(𝜑𝑥 = 𝑦) ∧ ∀𝑥(𝜓𝑥 = 𝑧) ∧ 𝜒)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

20.29.5  Set Theory

Theoremelnev 38459* 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 38460 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 38461 Equivalence between two ways of saying "is a member of the complement of 𝐴." (Contributed by Andrew Salmon, 15-Jul-2011.)
(𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥𝐴)

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

Theoremcompne 38463 The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.)
(V ∖ 𝐴) ≠ 𝐴

TheoremcompneOLD 38464 Obsolete proof of compne 38463 as of 11-Nov-2021. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(V ∖ 𝐴) ≠ 𝐴

Theoremcompab 38465 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 38466 Obsolete proof of complss 3743 as of 7-Aug-2021. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴))

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

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

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

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

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

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

Theoremipo0 38473 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 38474 A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.)
( I Fr 𝐴𝐴 = ∅)

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

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

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

Theoremxpexb 38478 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 38479 An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5088, ax-reg 8482 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.)
((Tr 𝐴𝐵𝐴) → 𝐵𝐴)

20.29.6  Arithmetic

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

20.29.7  Geometry

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

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

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

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

Syntaxcrr3c 38485 RR3 is a class.
class RR3

Syntaxcline3 38486 line3 is a class.
class line3

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

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

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

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

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

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

Theoremaddrfv 38493 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 38494 Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)
((𝐴𝐸𝐵𝐷𝐶 ∈ ℝ) → ((𝐴-𝑟𝐵)‘𝐶) = ((𝐴𝐶) − (𝐵𝐶)))

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

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

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

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