P. 449 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44801-44900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pm11.11 44801	Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ 𝜑    ⇒   ⊢ ∀𝑧∀𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
Theorem	pm11.12 44802*	Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥∀𝑦𝜓))
Theorem	19.21vv 44803*	Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1941. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜓 → 𝜑) ↔ (𝜓 → ∀𝑥∀𝑦𝜑))
Theorem	2alim 44804	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 44805	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 44806	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 44807	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 44808	Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑥∃𝑦𝜑)
Theorem	19.33-2 44809	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 44810*	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 44811*	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 44812*	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 44813*	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 44814	Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥∀𝑦(𝜑 → ¬ 𝜓))
Theorem	aaanv 44815*	Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2338. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥𝜑 ∧ ∀𝑦𝜓) ↔ ∀𝑥∀𝑦(𝜑 ∧ 𝜓))
Theorem	pm11.57 44816*	Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.58 44817*	Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.59 44818*	Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑦∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜓 ∧ [𝑦 / 𝑥]𝜓)))
Theorem	pm11.6 44819*	Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ∃𝑦(∃𝑥(𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	pm11.61 44820*	Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → ∃𝑦𝜓))
Theorem	pm11.62 44821*	Theorem *11.62 in [WhiteheadRussell] p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝜒) ↔ ∀𝑥(𝜑 → ∀𝑦(𝜓 → 𝜒)))
Theorem	pm11.63 44822	Theorem *11.63 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥∃𝑦𝜑 → ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	pm11.7 44823	Theorem *11.7 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜑) ↔ ∃𝑥∃𝑦𝜑)
Theorem	pm11.71 44824*	Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑦(𝜒 → 𝜃)) ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))))
21.40.3  Predicate Calculus
Theorem	sbeqal1 44825*	If 𝑥 = 𝑦 always implies 𝑥 = 𝑧, then 𝑦 = 𝑧. (Contributed by Andrew Salmon, 2-Jun-2011.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧) → 𝑦 = 𝑧)
Theorem	sbeqal1i 44826*	Suppose you know 𝑥 = 𝑦 implies 𝑥 = 𝑧, assuming 𝑥 and 𝑧 are distinct. Then, 𝑦 = 𝑧. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧)    ⇒   ⊢ 𝑦 = 𝑧
Theorem	sbeqal2i 44827*	If 𝑥 = 𝑦 implies 𝑥 = 𝑧, then we can infer 𝑧 = 𝑦. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧)    ⇒   ⊢ 𝑧 = 𝑦
Theorem	axc5c4c711 44828	Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1797 as the inference rule. This proof extends the idea of axc5c711 39364 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.)
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦(∀𝑦𝜑 → 𝜓) → (𝜑 → ∀𝑦(∀𝑦𝜑 → 𝜓))) → (∀𝑦𝜑 → ∀𝑦𝜓))
Theorem	axc5c4c711toc5 44829	Rederivation of sp 2191 from axc5c4c711 44828. Note that ax6 2389 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1970 instead of ax6 2389, so that this rederivation requires only ax6v 1970 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c4c711toc4 44830	Rederivation of axc4 2327 from axc5c4c711 44828. 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 44831	Rederivation of axc7 2323 from axc5c4c711 44828. Note that neither axc7 2323 nor ax-11 2163 are required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c4c711to11 44832	Rederivation of ax-11 2163 from axc5c4c711 44828. Note that ax-11 2163 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	axc11next 44833*	This theorem shows that, given axextb 2712, 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.)
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)
21.40.4  Principia Mathematica * 13 and * 14
Theorem	pm13.13a 44834	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 44835	Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (([𝐴 / 𝑥]𝜑 ∧ 𝑥 = 𝐴) → 𝜑)
Theorem	pm13.14 44836	Theorem *13.14 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (([𝐴 / 𝑥]𝜑 ∧ ¬ 𝜑) → 𝑥 ≠ 𝐴)
Theorem	pm13.192 44837*	Theorem *13.192 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
⊢ (∃𝑦(∀𝑥(𝑥 = 𝐴 ↔ 𝑥 = 𝑦) ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑)
Theorem	pm13.193 44838	Theorem *13.193 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝑥 = 𝑦))
Theorem	pm13.194 44839	Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝜑 ∧ 𝑥 = 𝑦))
Theorem	pm13.195 44840*	Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3757. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑)
Theorem	pm13.196a 44841*	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 44842*	Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑧∀𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))
Theorem	2sbc5g 44843*	Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))
Theorem	iotain 44844	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} = (℩𝑥𝜑))
Theorem	iotaexeu 44845	The iota class exists. This theorem does not require ax-nul 5242 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
Theorem	iotasbc 44846*	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 44847*	Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ ((∃!𝑥𝜑 ∧ ∃!𝑥𝜓) → ([(℩𝑥𝜑) / 𝑦][(℩𝑥𝜓) / 𝑧]𝜒 ↔ ∃𝑦∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∀𝑥(𝜓 ↔ 𝑥 = 𝑧) ∧ 𝜒)))
Theorem	pm14.12 44848*	Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	pm14.122a 44849*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑)))
Theorem	pm14.122b 44850*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑)))
Theorem	pm14.122c 44851*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑)))
Theorem	pm14.123a 44852*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)))
Theorem	pm14.123b 44853*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑)))
Theorem	pm14.123c 44854*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑)))
Theorem	pm14.18 44855	Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥𝜓 → [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	iotaequ 44856*	Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (℩𝑥𝑥 = 𝑦) = 𝑦
Theorem	iotavalb 44857*	Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 6473. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (℩𝑥𝜑) = 𝑦))
Theorem	iotasbc5 44858*	Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(𝑦 = (℩𝑥𝜑) ∧ 𝜓)))
Theorem	pm14.24 44859*	Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑)))
Theorem	iotavalsb 44860*	Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([𝑦 / 𝑧]𝜓 ↔ [(℩𝑥𝜑) / 𝑧]𝜓))
Theorem	sbiota1 44861	Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	sbaniota 44862	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	iotasbcq 44863	Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([(℩𝑥𝜑) / 𝑦]𝜒 ↔ [(℩𝑥𝜓) / 𝑦]𝜒))
21.40.5  Set Theory
Theorem	elnev 44864*	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 44865	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 44866*	Equality between two ways of saying "the complement of 𝐴". (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (V ∖ 𝐴) = {𝑥 ∣ ¬ 𝑥 ∈ 𝐴}
Theorem	compne 44867	The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.)
⊢ (V ∖ 𝐴) ≠ 𝐴
Theorem	compab 44868	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 44869	Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (𝐴 ⊆ (V ∖ 𝐵) ↔ 𝐵 ⊆ (V ∖ 𝐴))
Theorem	conss1 44870	Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ ((V ∖ 𝐴) ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ 𝐴)
Theorem	ralbidar 44871	More general form of ralbida 3249. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidar 44872	More general form of rexbida 3250. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	dropab1 44873	Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑥, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ 𝜑})
Theorem	dropab2 44874	Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑧, 𝑥⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜑})
Theorem	ipo0 44875	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 44876	A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅)
Theorem	ordpss 44877	ordelpss 6352 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵))
Theorem	fvsb 44878*	Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (∃!𝑦 𝐴𝐹𝑦 → ([(𝐹‘𝐴) / 𝑥]𝜑 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))
Theorem	fveqsb 44879*	Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (𝑥 = (𝐹‘𝐴) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃!𝑦 𝐴𝐹𝑦 → (𝜓 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))
Theorem	xpexb 44880	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 44881	An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5614, ax-reg 9507 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.)
⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊊ 𝐴)
21.40.6  Arithmetic
Theorem	addcomgi 44882	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.40.7  Geometry
Syntax	cplusr 44883	Introduce the operation of vector addition.
class +𝑟
Syntax	cminusr 44884	Introduce the operation of vector subtraction.
class -𝑟
Syntax	ctimesr 44885	Introduce the operation of scalar multiplication.
class .𝑣
Syntax	cptdfc 44886	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 44887	RR3 is a class.
class RR3
Syntax	cline3 44888	line3 is a class.
class line3
Definition	df-addr 44889*	Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ +𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) + (𝑦‘𝑣))))
Definition	df-subr 44890*	Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ -𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣))))
Definition	df-mulv 44891*	Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ .𝑣 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ (𝑥 · (𝑦‘𝑣))))
Theorem	addrval 44892*	Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) + (𝐵‘𝑣))))
Theorem	subrval 44893*	Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) − (𝐵‘𝑣))))
Theorem	mulvval 44894*	Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) = (𝑣 ∈ ℝ ↦ (𝐴 · (𝐵‘𝑣))))
Theorem	addrfv 44895	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 44896	Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴-𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) − (𝐵‘𝐶)))
Theorem	mulvfv 44897	Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴.𝑣𝐵)‘𝐶) = (𝐴 · (𝐵‘𝐶)))
Theorem	addrfn 44898	Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) Fn ℝ)
Theorem	subrfn 44899	Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) Fn ℝ)
Theorem	mulvfn 44900	Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) Fn ℝ)