P. 363 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36201-36300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ax12fromc15 36201	Rederivation of axiom ax-12 2175 from ax-c15 36185, ax-c11 36183 (used through dral1-o 36200), and other older axioms. See theorem axc15 2433 for the derivation of ax-c15 36185 from ax-12 2175. An open problem is whether we can prove this using ax-c11n 36184 instead of ax-c11 36183. This proof uses newer axioms ax-4 1811 and ax-6 1970, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 36180 and ax-c10 36182. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax13fromc9 36202	Derive ax-13 2379 from ax-c9 36186 and other older axioms. This proof uses newer axioms ax-4 1811 and ax-6 1970, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 36180 and ax-c10 36182. (Contributed by NM, 21-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
20.24.3  Legacy theorems using obsolete axioms These theorems were mostly intended to study properties of the older axiom schemes and are not useful outside of this section. They should not be used outside of this section. They may be deleted when they are deemed to no longer be of interest.
Theorem	ax5ALT 36203*	Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113. (This theorem simply repeats ax-5 1911 so that we can include the following note, which applies only to the obsolete axiomatization.) This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1797, ax-c4 36180, ax-c5 36179, ax-11 2158, ax-c7 36181, ax-7 2015, ax-c9 36186, ax-c10 36182, ax-c11 36183, ax-8 2113, ax-9 2121, ax-c14 36187, ax-c15 36185, and ax-c16 36188: in that system, we can derive any instance of ax-5 1911 not containing wff variables by induction on formula length, using ax5eq 36228 and ax5el 36233 for the basis together with hbn 2299, hbal 2171, and hbim 2303. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). (Contributed by NM, 19-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)
Theorem	sps-o 36204	Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	hbequid 36205	Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof does not use ax-c10 36182.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
Theorem	nfequid-o 36206	Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof uses only ax-4 1811, ax-7 2015, ax-c9 36186, and ax-gen 1797. This shows that this can be proved without ax6 2391, even though the theorem equid 2019 cannot be. A shorter proof using ax6 2391 is obtainable from equid 2019 and hbth 1805.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 1971, which is used for the derivation of axc9 2389, unless we consider ax-c9 36186 the starting axiom rather than ax-13 2379. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑦 𝑥 = 𝑥
Theorem	axc5c7 36207	Proof of a single axiom that can replace ax-c5 36179 and ax-c7 36181. See axc5c7toc5 36208 and axc5c7toc7 36209 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c7toc5 36208	Rederivation of ax-c5 36179 from axc5c7 36207. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c7toc7 36209	Rederivation of ax-c7 36181 from axc5c7 36207. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc711 36210	Proof of a single axiom that can replace both ax-c7 36181 and ax-11 2158. See axc711toc7 36212 and axc711to11 36213 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑)
Theorem	nfa1-o 36211	𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	axc711toc7 36212	Rederivation of ax-c7 36181 from axc711 36210. Note that ax-c7 36181 and ax-11 2158 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc711to11 36213	Rederivation of ax-11 2158 from axc711 36210. Note that ax-c7 36181 and ax-11 2158 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	axc5c711 36214	Proof of a single axiom that can replace ax-c5 36179, ax-c7 36181, and ax-11 2158 in a subsystem that includes these axioms plus ax-c4 36180 and ax-gen 1797 (and propositional calculus). See axc5c711toc5 36215, axc5c711toc7 36216, and axc5c711to11 36217 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 36207. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c711toc5 36215	Rederivation of ax-c5 36179 from axc5c711 36214. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c711toc7 36216	Rederivation of ax-c7 36181 from axc5c711 36214. Note that ax-c7 36181 and ax-11 2158 are not used by the rederivation. The use of alimi 1813 (which uses ax-c5 36179) is allowed since we have already proved axc5c711toc5 36215. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c711to11 36217	Rederivation of ax-11 2158 from axc5c711 36214. Note that ax-c7 36181 and ax-11 2158 are not used by the rederivation. The use of alimi 1813 (which uses ax-c5 36179) is allowed since we have already proved axc5c711toc5 36215. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	equidqe 36218	equid 2019 with existential quantifier without using ax-c5 36179 or ax-5 1911. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥
Theorem	axc5sp1 36219	A special case of ax-c5 36179 without using ax-c5 36179 or ax-5 1911. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥)
Theorem	equidq 36220	equid 2019 with universal quantifier without using ax-c5 36179 or ax-5 1911. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∀𝑦 𝑥 = 𝑥
Theorem	equid1ALT 36221	Alternate proof of equid 2019 and equid1 36195 from older axioms ax-c7 36181, ax-c10 36182 and ax-c9 36186. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	axc11nfromc11 36222	Rederivation of ax-c11n 36184 from original version ax-c11 36183. See theorem axc11 2441 for the derivation of ax-c11 36183 from ax-c11n 36184. This theorem should not be referenced in any proof. Instead, use ax-c11n 36184 above so that uses of ax-c11n 36184 can be more easily identified, or use aecom-o 36197 when this form is needed for studies involving ax-c11 36183 and omitting ax-5 1911. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	naecoms-o 36223	A commutation rule for distinct variable specifiers. Version of naecoms 2440 using ax-c11 36183. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbnae-o 36224	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2443 using ax-c11 36183. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	dvelimf-o 36225	Proof of dvelimh 2461 that uses ax-c11 36183 but not ax-c15 36185, ax-c11n 36184, or ax-12 2175. Version of dvelimh 2461 using ax-c11 36183 instead of axc11 2441. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dral2-o 36226	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral2 2449 using ax-c11 36183. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))
Theorem	aev-o 36227*	A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-c16 36188. Version of aev 2062 using ax-c11 36183. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣)
Theorem	ax5eq 36228*	Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1911 considered as a metatheorem. Do not use it for later proofs - use ax-5 1911 instead, to avoid reference to the redundant axiom ax-c16 36188.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
Theorem	dveeq2-o 36229*	Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2385 using ax-c15 36185. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	axc16g-o 36230*	A generalization of axiom ax-c16 36188. Version of axc16g 2258 using ax-c11 36183. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	dveeq1-o 36231*	Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2387 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	dveeq1-o16 36232*	Version of dveeq1 2387 using ax-c16 36188 instead of ax-5 1911. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1911. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax5el 36233*	Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1911 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)
Theorem	axc11n-16 36234*	This theorem shows that, given ax-c16 36188, we can derive a version of ax-c11n 36184. However, it is weaker than ax-c11n 36184 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)
Theorem	dveel2ALT 36235*	Alternate proof of dveel2 2474 using ax-c16 36188 instead of ax-5 1911. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
Theorem	ax12f 36236	Basis step for constructing a substitution instance of ax-c15 36185 without using ax-c15 36185. We can start with any formula 𝜑 in which 𝑥 is not free. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12eq 36237	Basis step for constructing a substitution instance of ax-c15 36185 without using ax-c15 36185. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
Theorem	ax12el 36238	Basis step for constructing a substitution instance of ax-c15 36185 without using ax-c15 36185. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
Theorem	ax12indn 36239	Induction step for constructing a substitution instance of ax-c15 36185 without using ax-c15 36185. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑))))
Theorem	ax12indi 36240	Induction step for constructing a substitution instance of ax-c15 36185 without using ax-c15 36185. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜓 → ∀𝑥(𝑥 = 𝑦 → 𝜓))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → ((𝜑 → 𝜓) → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))))
Theorem	ax12indalem 36241	Lemma for ax12inda2 36243 and ax12inda 36244. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
Theorem	ax12inda2ALT 36242*	Alternate proof of ax12inda2 36243, slightly more direct and not requiring ax-c16 36188. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Theorem	ax12inda2 36243*	Induction step for constructing a substitution instance of ax-c15 36185 without using ax-c15 36185. Quantification case. When 𝑧 and 𝑦 are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 36244. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Theorem	ax12inda 36244*	Induction step for constructing a substitution instance of ax-c15 36185 without using ax-c15 36185. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 36243 may be used instead to avoid the dummy variable 𝑤 in the proof.) (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (𝜑 → ∀𝑥(𝑥 = 𝑤 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Theorem	ax12v2-o 36245*	Rederivation of ax-c15 36185 from ax12v 2176 (without using ax-c15 36185 or the full ax-12 2175). Thus, the hypothesis (ax12v 2176) provides an alternate axiom that can be used in place of ax-c15 36185. See also axc15 2433. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12a2-o 36246*	Derive ax-c15 36185 from a hypothesis in the form of ax-12 2175, without using ax-12 2175 or ax-c15 36185. The hypothesis is weaker than ax-12 2175, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2175, if we also have ax-c11 36183, which this proof uses. As theorem ax12 2434 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 36184 instead of ax-c11 36183. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	axc11-o 36247	Show that ax-c11 36183 can be derived from ax-c11n 36184 and ax-12 2175. An open problem is whether this theorem can be derived from ax-c11n 36184 and the others when ax-12 2175 is replaced with ax-c15 36185 or ax12v 2176. See theorem axc11nfromc11 36222 for the rederivation of ax-c11n 36184 from axc11 2441. Normally, axc11 2441 should be used rather than ax-c11 36183 or axc11-o 36247, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	fsumshftd 36248*	Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15127. The proof demonstrates how this can be derived starting from from fsumshft 15127. (Contributed by NM, 1-Nov-2019.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑗 = (𝑘 − 𝐾)) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵)
Axiom	ax-riotaBAD 36249	Define restricted description binder. In case it doesn't exist, we return a set which is not a member of the domain of discourse 𝐴. See also comments for df-iota 6283. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7093, CONFLICTS WITH (THE NEW) df-riota 7093 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED.
⊢ (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴}))
Theorem	riotaclbgBAD 36250*	Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴))
Theorem	riotaclbBAD 36251*	Closure of restricted iota. (Contributed by NM, 15-Sep-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)
Theorem	riotasvd 36252*	Deduction version of riotasv 36255. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶)))    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝐷 = 𝐶))
Theorem	riotasv2d 36253*	Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5269). Special case of riota2f 7117. (Contributed by NM, 2-Mar-2013.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝐹)    &   ⊢ (𝜑 → Ⅎ𝑦𝜒)    &   ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶)))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → 𝐶 = 𝐹)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝐷 = 𝐹)
Theorem	riotasv2s 36254*	The value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5269) in the form of a substitution instance. Special case of riota2f 7117. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ (𝐸 ∈ 𝐵 ∧ [𝐸 / 𝑦]𝜑)) → 𝐷 = ⦋𝐸 / 𝑦⦌𝐶)
Theorem	riotasv 36255*	Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5269). Special case of riota2f 7117. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))    ⇒   ⊢ ((𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐷 = 𝐶)
Theorem	riotasv3d 36256*	A property 𝜒 holding for a representative of a single-valued class expression 𝐶(𝑦) (see e.g. reusv2 5269) also holds for its description binder 𝐷 (in the form of property 𝜃). (Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜃)    &   ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶)))    &   ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝜒))    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝜃)
20.24.4  Experiments with weak deduction theorem
Theorem	elimhyps 36257	A version of elimhyp 4488 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
⊢ [𝐵 / 𝑥]𝜑    ⇒   ⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜑
Theorem	dedths 36258	A version of weak deduction theorem dedth 4481 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜓    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	renegclALT 36259	Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 10938. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
Theorem	elimhyps2 36260	Generalization of elimhyps 36257 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.)
⊢ [𝐵 / 𝑥]𝜑    ⇒   ⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜑
Theorem	dedths2 36261	Generalization of dedths 36258 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.)
⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜓    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓)
Theorem	nfcxfrdf 36262	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐴)
Theorem	nfded 36263	A deduction theorem that converts a not-free inference directly to deduction form. The first hypothesis is the hypothesis of the deduction form. The second is an equality deduction (e.g., (Ⅎ𝑥𝐴 → ∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴} = ∪ 𝐴)) that starts from abidnf 3642. The last is assigned to the inference form (e.g., Ⅎ𝑥∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}) whose hypothesis is satisfied using nfaba1 2963. (Contributed by NM, 19-Nov-2020.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (Ⅎ𝑥𝐴 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐶)
Theorem	nfded2 36264	A deduction theorem that converts a not-free inference directly to deduction form. The first 2 hypotheses are the hypotheses of the deduction form. The third is an equality deduction (e.g., ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → ⟨{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}⟩ = ⟨𝐴, 𝐵⟩) for nfopd 4782) that starts from abidnf 3642. The last is assigned to the inference form (e.g., Ⅎ𝑥⟨{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}⟩ for nfop 4781) whose hypotheses are satisfied using nfaba1 2963. (Contributed by NM, 19-Nov-2020.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    &   ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 𝐶 = 𝐷)    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝐷)
Theorem	nfunidALT2 36265	Deduction version of nfuni 4807. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	nfunidALT 36266	Deduction version of nfuni 4807. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	nfopdALT 36267	Deduction version of bound-variable hypothesis builder nfop 4781. This shows how the deduction version of a not-free theorem such as nfop 4781 can be created from the corresponding not-free inference theorem. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⟨𝐴, 𝐵⟩)
20.24.5  Miscellanea
Theorem	cnaddcom 36268	Recover the commutative law of addition for complex numbers from the Abelian group structure. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	toycom 36269*	Show the commutative law for an operation 𝑂 on a toy structure class 𝐶 of commuatitive operations on ℂ. This illustrates how a structure class can be partially specialized. In practice, we would ordinarily define a new constant such as "CAbel" in place of 𝐶. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.)
⊢ 𝐶 = {𝑔 ∈ Abel ∣ (Base‘𝑔) = ℂ}    &   ⊢ + = (+g‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
20.24.6  Atoms, hyperplanes, and covering in a left vector space (or module)
Syntax	clsa 36270	Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space.
class LSAtoms
Syntax	clsh 36271	Extend class notation with all subspaces of a left module or left vector space that are hyperplanes.
class LSHyp
Definition	df-lsatoms 36272*	Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.)
⊢ LSAtoms = (𝑤 ∈ V ↦ ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})))
Definition	df-lshyp 36273*	Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less that the full space. (Contributed by NM, 29-Jun-2014.)
⊢ LSHyp = (𝑤 ∈ V ↦ {𝑠 ∈ (LSubSp‘𝑤) ∣ (𝑠 ≠ (Base‘𝑤) ∧ ∃𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤))})
Theorem	lshpset 36274*	The set of all hyperplanes of a left module or left vector space. The vector 𝑣 is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝐻 = {𝑠 ∈ 𝑆 ∣ (𝑠 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑁‘(𝑠 ∪ {𝑣})) = 𝑉)})
Theorem	islshp 36275*	The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑁‘(𝑈 ∪ {𝑣})) = 𝑉)))
Theorem	islshpsm 36276*	Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉)))
Theorem	lshplss 36277	A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	lshpne 36278	A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → 𝑈 ≠ 𝑉)
Theorem	lshpnel 36279	A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)
Theorem	lshpnelb 36280	The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (¬ 𝑋 ∈ 𝑈 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉))
Theorem	lshpnel2N 36281	Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑈 ≠ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉))
Theorem	lshpne0 36282	The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014.) (Proof shortened by AV, 19-Jul-2022.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 0 )
Theorem	lshpdisj 36283	A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)    ⇒   ⊢ (𝜑 → (𝑈 ∩ (𝑁‘{𝑋})) = { 0 })
Theorem	lshpcmp 36284	If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lshpinN 36285	The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.)
⊢ 𝐻 = (LSHyp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐻)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐻)    ⇒   ⊢ (𝜑 → ((𝑇 ∩ 𝑈) ∈ 𝐻 ↔ 𝑇 = 𝑈))
Theorem	lsatset 36286*	The set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝐴 = ran (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})))
Theorem	islsat 36287*	The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑈 = (𝑁‘{𝑥})))
Theorem	lsatlspsn2 36288	The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 36289 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) ∈ 𝐴)
Theorem	lsatlspsn 36289	The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))    ⇒   ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ 𝐴)
Theorem	islsati 36290*	A 1-dim subspace (atom) (of a left module or left vector space) equals the span of some vector. (Contributed by NM, 1-Oct-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑈 ∈ 𝐴) → ∃𝑣 ∈ 𝑉 𝑈 = (𝑁‘{𝑣}))
Theorem	lsateln0 36291*	A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ 𝑈 𝑣 ≠ 0 )
Theorem	lsatlss 36292	The set of 1-dim subspaces is a set of subspaces. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → 𝐴 ⊆ 𝑆)
Theorem	lsatlssel 36293	An atom is a subspace. (Contributed by NM, 25-Aug-2014.)
⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	lsatssv 36294	An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑄 ⊆ 𝑉)
Theorem	lsatn0 36295	A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 30128 analog.) (Contributed by NM, 25-Aug-2014.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑈 ≠ { 0 })
Theorem	lsatspn0 36296	The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∈ 𝐴 ↔ 𝑋 ≠ 0 ))
Theorem	lsator0sp 36297	The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑁‘{𝑋}) ∈ 𝐴 ∨ (𝑁‘{𝑋}) = { 0 }))
Theorem	lsatssn0 36298	A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑈 ≠ { 0 })
Theorem	lsatcmp 36299	If two atoms are comparable, they are equal. (atsseq 30130 analog.) TODO: can lspsncmp 19881 shorten this? (Contributed by NM, 25-Aug-2014.)
⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))
Theorem	lsatcmp2 36300	If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 36299. TODO: can lspsncmp 19881 shorten this? (Contributed by NM, 3-Feb-2015.)
⊢ 0 = (0g‘𝑊)    &   ⊢ 𝐴 = (LSAtoms‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∨ 𝑈 = { 0 }))    ⇒   ⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))