P. 390 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38901-39000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	19.37vv 38901*	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 38902*	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 38903	Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥∀𝑦(𝜑 → ¬ 𝜓))
Theorem	2exanali 38904	Theorem *11.521 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥∃𝑦(𝜑 ∧ ¬ 𝜓) ↔ ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	aaanv 38905*	Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2206. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥𝜑 ∧ ∀𝑦𝜓) ↔ ∀𝑥∀𝑦(𝜑 ∧ 𝜓))
Theorem	pm11.57 38906*	Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.58 38907*	Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.59 38908*	Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑦∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜓 ∧ [𝑦 / 𝑥]𝜓)))
Theorem	pm11.6 38909*	Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ∃𝑦(∃𝑥(𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	pm11.61 38910*	Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → ∃𝑦𝜓))
Theorem	pm11.62 38911*	Theorem *11.62 in [WhiteheadRussell] p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝜒) ↔ ∀𝑥(𝜑 → ∀𝑦(𝜓 → 𝜒)))
Theorem	pm11.63 38912	Theorem *11.63 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥∃𝑦𝜑 → ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	pm11.7 38913	Theorem *11.7 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜑) ↔ ∃𝑥∃𝑦𝜑)
Theorem	pm11.71 38914*	Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑦(𝜒 → 𝜃)) ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))))
20.30.3  Predicate Calculus
Theorem	sbeqal1 38915*	If 𝑥 = 𝑦 always implies 𝑥 = 𝑧, then 𝑦 = 𝑧 is true. (Contributed by Andrew Salmon, 2-Jun-2011.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧) → 𝑦 = 𝑧)
Theorem	sbeqal1i 38916*	Suppose you know 𝑥 = 𝑦 implies 𝑥 = 𝑧, assuming 𝑥 and 𝑧 are distinct. Then, 𝑦 = 𝑧. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧)    ⇒   ⊢ 𝑦 = 𝑧
Theorem	sbeqal2i 38917*	If 𝑥 = 𝑦 implies 𝑥 = 𝑧, then we can infer 𝑧 = 𝑦. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧)    ⇒   ⊢ 𝑧 = 𝑦
Theorem	sbeqalbi 38918*	When both 𝑥 and 𝑧 and 𝑦 and 𝑧 are both distinct, then the converse of sbeqal1 holds as well. (Contributed by Andrew Salmon, 2-Jun-2011.)
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 = 𝑥 → 𝑧 = 𝑦))
Theorem	axc5c4c711 38919	Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1762 as the inference rule. This proof extends the idea of axc5c711 34522 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.)
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦(∀𝑦𝜑 → 𝜓) → (𝜑 → ∀𝑦(∀𝑦𝜑 → 𝜓))) → (∀𝑦𝜑 → ∀𝑦𝜓))
Theorem	axc5c4c711toc5 38920	Rederivation of sp 2091 from axc5c4c711 38919. Note that ax6 2287 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1946 instead of ax6 2287, so that this rederivation requires only ax6v 1946 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c4c711toc4 38921	Rederivation of axc4 2168 from axc5c4c711 38919. 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 38922	Rederivation of axc7 2170 from axc5c4c711 38919. Note that neither axc7 2170 nor ax-11 2074 are required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c4c711to11 38923	Rederivation of ax-11 2074 from axc5c4c711 38919. Note that ax-11 2074 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	axc11next 38924*	This theorem shows that, given axext4 2635, we can derive a version of axc11n 2342. However, it is weaker than axc11n 2342 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)
20.30.4  Principia Mathematica * 13 and * 14
Theorem	pm13.13a 38925	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 38926	Theorem *13.13 in [WhiteheadRussell] p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (([𝐴 / 𝑥]𝜑 ∧ 𝑥 = 𝐴) → 𝜑)
Theorem	pm13.14 38927	Theorem *13.14 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (([𝐴 / 𝑥]𝜑 ∧ ¬ 𝜑) → 𝑥 ≠ 𝐴)
Theorem	pm13.192 38928*	Theorem *13.192 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
⊢ (∃𝑦(∀𝑥(𝑥 = 𝐴 ↔ 𝑥 = 𝑦) ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑)
Theorem	pm13.193 38929	Theorem *13.193 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝑥 = 𝑦))
Theorem	pm13.194 38930	Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝜑 ∧ 𝑥 = 𝑦))
Theorem	pm13.195 38931*	Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3493. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑)
Theorem	pm13.196a 38932*	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 38933*	Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑧∀𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))
Theorem	2sbc5g 38934*	Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))
Theorem	iotain 38935	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} = (℩𝑥𝜑))
Theorem	iotaexeu 38936	The iota class exists. This theorem does not require ax-nul 4822 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
Theorem	iotasbc 38937*	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 38938*	Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ ((∃!𝑥𝜑 ∧ ∃!𝑥𝜓) → ([(℩𝑥𝜑) / 𝑦][(℩𝑥𝜓) / 𝑧]𝜒 ↔ ∃𝑦∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∀𝑥(𝜓 ↔ 𝑥 = 𝑧) ∧ 𝜒)))
Theorem	pm14.12 38939*	Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	pm14.122a 38940*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑)))
Theorem	pm14.122b 38941*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑)))
Theorem	pm14.122c 38942*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑)))
Theorem	pm14.123a 38943*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)))
Theorem	pm14.123b 38944*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑)))
Theorem	pm14.123c 38945*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑)))
Theorem	pm14.18 38946	Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥𝜓 → [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	iotaequ 38947*	Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (℩𝑥𝑥 = 𝑦) = 𝑦
Theorem	iotavalb 38948*	Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 5900. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (℩𝑥𝜑) = 𝑦))
Theorem	iotasbc5 38949*	Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(𝑦 = (℩𝑥𝜑) ∧ 𝜓)))
Theorem	pm14.24 38950*	Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑)))
Theorem	iotavalsb 38951*	Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([𝑦 / 𝑧]𝜓 ↔ [(℩𝑥𝜑) / 𝑧]𝜓))
Theorem	sbiota1 38952	Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	sbaniota 38953	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	eubi 38954	Theorem *14.271 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
Theorem	iotasbcq 38955	Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([(℩𝑥𝜑) / 𝑦]𝜒 ↔ [(℩𝑥𝜓) / 𝑦]𝜒))
20.30.5  Set Theory
Theorem	elnev 38956*	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 38957	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	compel 38958	Equivalence between two ways of saying "is a member of the complement of 𝐴." (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴)
Theorem	compeq 38959*	Equality between two ways of saying "the complement of 𝐴." (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (V ∖ 𝐴) = {𝑥 ∣ ¬ 𝑥 ∈ 𝐴}
Theorem	compne 38960	The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.)
⊢ (V ∖ 𝐴) ≠ 𝐴
Theorem	compneOLD 38961	Obsolete proof of compne 38960 as of 11-Nov-2021. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (V ∖ 𝐴) ≠ 𝐴
Theorem	compab 38962	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	conss34OLD 38963	Obsolete proof of complss 3784 as of 7-Aug-2021. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴))
Theorem	conss2 38964	Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (𝐴 ⊆ (V ∖ 𝐵) ↔ 𝐵 ⊆ (V ∖ 𝐴))
Theorem	conss1 38965	Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ ((V ∖ 𝐴) ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ 𝐴)
Theorem	ralbidar 38966	More general form of ralbida 3011. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidar 38967	More general form of rexbida 3076. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	dropab1 38968	Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑥, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ 𝜑})
Theorem	dropab2 38969	Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑧, 𝑥⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜑})
Theorem	ipo0 38970	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 38971	A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅)
Theorem	ordpss 38972	ordelpss 5789 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵))
Theorem	fvsb 38973*	Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (∃!𝑦 𝐴𝐹𝑦 → ([(𝐹‘𝐴) / 𝑥]𝜑 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))
Theorem	fveqsb 38974*	Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (𝑥 = (𝐹‘𝐴) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃!𝑦 𝐴𝐹𝑦 → (𝜓 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))
Theorem	xpexb 38975	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 38976	An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5127, ax-reg 8538 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.)
⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊊ 𝐴)
20.30.6  Arithmetic
Theorem	addcomgi 38977	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.30.7  Geometry
Syntax	cplusr 38978	Introduce the operation of vector addition.
class +𝑟
Syntax	cminusr 38979	Introduce the operation of vector subtraction.
class -𝑟
Syntax	ctimesr 38980	Introduce the operation of scalar multiplication.
class .𝑣
Syntax	cptdfc 38981	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 38982	RR3 is a class.
class RR3
Syntax	cline3 38983	line3 is a class.
class line3
Definition	df-addr 38984*	Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ +𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) + (𝑦‘𝑣))))
Definition	df-subr 38985*	Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ -𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣))))
Definition	df-mulv 38986*	Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ .𝑣 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ (𝑥 · (𝑦‘𝑣))))
Theorem	addrval 38987*	Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) + (𝐵‘𝑣))))
Theorem	subrval 38988*	Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) − (𝐵‘𝑣))))
Theorem	mulvval 38989*	Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) = (𝑣 ∈ ℝ ↦ (𝐴 · (𝐵‘𝑣))))
Theorem	addrfv 38990	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 38991	Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴-𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) − (𝐵‘𝐶)))
Theorem	mulvfv 38992	Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴.𝑣𝐵)‘𝐶) = (𝐴 · (𝐵‘𝐶)))
Theorem	addrfn 38993	Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) Fn ℝ)
Theorem	subrfn 38994	Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) Fn ℝ)
Theorem	mulvfn 38995	Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) Fn ℝ)
Theorem	addrcom 38996	Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝐵+𝑟𝐴))
Definition	df-ptdf 38997*	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 38998	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 = (ℝ ↑𝑚 {1, 2, 3})
Definition	df-line3 38999*	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 ∣ (2𝑜 ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))}
20.31  Mathbox for Alan Sare 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 7525 in 2008. He developed a tool called "completeusersproof" that assists developing proofs using his "virtual deduction" method: http://us.metamath.org/other.html#completeusersproof. His virtual deduction method is explained in the comment for wvd1 39102. 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....
20.31.1  Auxiliary theorems for the Virtual Deduction tool
Theorem	idiALT 39000	Placeholder for idi 2. 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.)
⊢ 𝜑    ⇒   ⊢ 𝜑