P. 65 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6401-6500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ordtr2 6401	Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ordtr3 6402	Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014.) (Proof shortened by JJ, 24-Sep-2021.)
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵)))
Theorem	ontr1 6403	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. Theorem 1.9(ii) of [Schloeder] p. 1. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ontr2 6404	Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	onelssex 6405*	Ordinal less than is equivalent to having an ordinal between them. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐶 ↔ ∃𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏))
Theorem	ordunidif 6406	The union of an ordinal stays the same if a subset equal to one of its elements is removed. (Contributed by NM, 10-Dec-2004.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴)
Theorem	ordintdif 6407	If 𝐵 is smaller than 𝐴, then it equals the intersection of the difference. Exercise 11 in [TakeutiZaring] p. 44. (Contributed by Andrew Salmon, 14-Nov-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵 ∧ (𝐴 ∖ 𝐵) ≠ ∅) → 𝐵 = ∩ (𝐴 ∖ 𝐵))
Theorem	onintss 6408*	If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ On → (𝜓 → ∩ {𝑥 ∈ On ∣ 𝜑} ⊆ 𝐴))
Theorem	oneqmini 6409*	A way to show that an ordinal number equals the minimum of a collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection. (Contributed by NM, 14-Nov-2003.)
⊢ (𝐵 ⊆ On → ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) → 𝐴 = ∩ 𝐵))
Theorem	ord0 6410	The empty set is an ordinal class. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 11-May-1994.)
⊢ Ord ∅
Theorem	0elon 6411	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 17-Sep-1993.)
⊢ ∅ ∈ On
Theorem	ord0eln0 6412	A nonempty ordinal contains the empty set. Lemma 1.10 of [Schloeder] p. 2. (Contributed by NM, 25-Nov-1995.)
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
Theorem	on0eln0 6413	An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004.)
⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
Theorem	dflim2 6414	An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))
Theorem	inton 6415	The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
⊢ ∩ On = ∅
Theorem	nlim0 6416	The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ¬ Lim ∅
Theorem	limord 6417	A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
⊢ (Lim 𝐴 → Ord 𝐴)
Theorem	limuni 6418	A limit ordinal is its own supremum (union). Lemma 2.13 of [Schloeder] p. 5. (Contributed by NM, 4-May-1995.)
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)
Theorem	limuni2 6419	The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
⊢ (Lim 𝐴 → Lim ∪ 𝐴)
Theorem	0ellim 6420	A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)
⊢ (Lim 𝐴 → ∅ ∈ 𝐴)
Theorem	limelon 6421	A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.)
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)
Theorem	onn0 6422	The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.)
⊢ On ≠ ∅
Theorem	suceqd 6423	Deduction associated with suceq 6424. (Contributed by Rohan Ridenour, 8-Aug-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → suc 𝐴 = suc 𝐵)
Theorem	suceq 6424	Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)
Theorem	elsuci 6425	Membership in a successor. This one-way implication does not require that either 𝐴 or 𝐵 be sets. Lemma 1.13 of [Schloeder] p. 2. (Contributed by NM, 6-Jun-1994.)
⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	elsucg 6426	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	elsuc2g 6427	Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	elsuc 6428	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	elsuc2 6429	Membership in a successor. (Contributed by NM, 15-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))
Theorem	nfsuc 6430	Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 suc 𝐴
Theorem	elelsuc 6431	Membership in a successor. (Contributed by NM, 20-Jun-1998.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵)
Theorem	sucel 6432*	Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.)
⊢ (suc 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)))
Theorem	suc0 6433	The successor of the empty set. (Contributed by NM, 1-Feb-2005.)
⊢ suc ∅ = {∅}
Theorem	sucprc 6434	A proper class is its own successor. (Contributed by NM, 3-Apr-1995.)
⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
Theorem	unisucs 6435	The union of the successor of a set is equal to the binary union of that set with its union. (Contributed by NM, 30-Aug-1993.) Extract from unisuc 6437. (Revised by BJ, 28-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → ∪ suc 𝐴 = (∪ 𝐴 ∪ 𝐴))
Theorem	unisucg 6436	A transitive class is equal to the union of its successor, closed form. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.) Generalize from unisuc 6437. (Revised by BJ, 28-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴))
Theorem	unisuc 6437	A transitive class is equal to the union of its successor, inference form. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴)
Theorem	sssucid 6438	A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)
⊢ 𝐴 ⊆ suc 𝐴
Theorem	sucidg 6439	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). Lemma 1.7 of [Schloeder] p. 1. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)
Theorem	sucid 6440	A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ suc 𝐴
Theorem	nsuceq0 6441	No successor is empty. (Contributed by NM, 3-Apr-1995.)
⊢ suc 𝐴 ≠ ∅
Theorem	eqelsuc 6442	A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵)
Theorem	iunsuc 6443*	Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ suc 𝐴𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶)
Theorem	suctr 6444	The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.) (Proof shortened by JJ, 24-Sep-2021.)
⊢ (Tr 𝐴 → Tr suc 𝐴)
Theorem	trsuc 6445	A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
Theorem	trsucss 6446	A member of the successor of a transitive class is a subclass of it. Lemma 1.13 of [Schloeder] p. 2. (Contributed by NM, 4-Oct-2003.)
⊢ (Tr 𝐴 → (𝐵 ∈ suc 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	ordsssuc 6447	An ordinal is a subset of another ordinal if and only if it belongs to its successor. (Contributed by NM, 28-Nov-2003.)
⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵))
Theorem	onsssuc 6448	A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵))
Theorem	ordsssuc2 6449	An ordinal subset of an ordinal number belongs to its successor. (Contributed by NM, 1-Feb-2005.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵))
Theorem	onmindif 6450	When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass. (Contributed by NM, 1-Dec-2003.)
⊢ ((𝐴 ⊆ On ∧ 𝐵 ∈ On) → 𝐵 ∈ ∩ (𝐴 ∖ suc 𝐵))
Theorem	ordnbtwn 6451	There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of [TakeutiZaring] p. 41. Lemma 1.15 of [Schloeder] p. 2. (Contributed by NM, 21-Jun-1998.) (Proof shortened by JJ, 24-Sep-2021.)
⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
Theorem	onnbtwn 6452	There is no set between an ordinal number and its successor. Proposition 7.25 of [TakeutiZaring] p. 41. Lemma 1.15 of [Schloeder] p. 2. (Contributed by NM, 9-Jun-1994.)
⊢ (𝐴 ∈ On → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
Theorem	sucssel 6453	A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.)
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
Theorem	orddif 6454	Ordinal derived from its successor. (Contributed by NM, 20-May-1998.)
⊢ (Ord 𝐴 → 𝐴 = (suc 𝐴 ∖ {𝐴}))
Theorem	orduniss 6455	An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.)
⊢ (Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴)
Theorem	ordtri2or 6456	A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	ordtri2or2 6457	A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	ordtri2or3 6458	A consequence of total ordering for ordinal classes. Similar to ordtri2or2 6457. (Contributed by David Moews, 1-May-2017.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = (𝐴 ∩ 𝐵) ∨ 𝐵 = (𝐴 ∩ 𝐵)))
Theorem	ordelinel 6459	The intersection of two ordinal classes is an element of a third if and only if either one of them is. (Contributed by David Moews, 1-May-2017.) (Proof shortened by JJ, 24-Sep-2021.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → ((𝐴 ∩ 𝐵) ∈ 𝐶 ↔ (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶)))
Theorem	ordssun 6460	Property of a subclass of the maximum (i.e. union) of two ordinals. (Contributed by NM, 28-Nov-2003.)
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶)))
Theorem	ordequn 6461	The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of [TakeutiZaring] p. 40. (Contributed by NM, 28-Nov-2003.)
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 = (𝐵 ∪ 𝐶) → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)))
Theorem	ordun 6462	The maximum (i.e., union) of two ordinals is ordinal. Exercise 12 of [TakeutiZaring] p. 40. (Contributed by NM, 28-Nov-2003.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∪ 𝐵))
Theorem	onunel 6463	The union of two ordinals is in a third iff both of the first two are. (Contributed by Scott Fenton, 10-Sep-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∪ 𝐵) ∈ 𝐶 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)))
Theorem	ordunisssuc 6464	A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003.)
⊢ ((𝐴 ⊆ On ∧ Ord 𝐵) → (∪ 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵))
Theorem	suc11 6465	The successor operation behaves like a one-to-one function. Compare Exercise 16 of [Enderton] p. 194. (Contributed by NM, 3-Sep-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵))
Theorem	onun2 6466	The union of two ordinals is an ordinal. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On)
Theorem	ontr 6467	An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.) Put in closed form. (Resised by BJ, 28-Dec-2024.)
⊢ (𝐴 ∈ On → Tr 𝐴)
Theorem	onunisuc 6468	An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) Generalize from onunisuci 6477. (Revised by BJ, 28-Dec-2024.)
⊢ (𝐴 ∈ On → ∪ suc 𝐴 = 𝐴)
Theorem	onordi 6469	An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ Ord 𝐴
Theorem	onirri 6470	An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ ¬ 𝐴 ∈ 𝐴
Theorem	oneli 6471	A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ On)
Theorem	onelssi 6472	A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)
Theorem	onssneli 6473	An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ∈ 𝐴)
Theorem	onssnel2i 6474	An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ⊆ 𝐴 → ¬ 𝐴 ∈ 𝐵)
Theorem	onelini 6475	An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴))
Theorem	oneluni 6476	An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴)
Theorem	onunisuci 6477	An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ ∪ suc 𝐴 = 𝐴
Theorem	onsseli 6478	Subset is equivalent to membership or equality for ordinal numbers. (Contributed by NM, 15-Sep-1995.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	onun2i 6479	The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    ⇒   ⊢ (𝐴 ∪ 𝐵) ∈ On
Theorem	unizlim 6480	An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴)))
Theorem	on0eqel 6481	An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004.)
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈ 𝐴))
Theorem	snsn0non 6482	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 7870). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 6483. (Contributed by NM, 21-May-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ ¬ {{∅}} ∈ On
Theorem	onxpdisj 6483	Ordinal numbers and ordered pairs are disjoint collections. This theorem can be used if we want to extend a set of ordinal numbers or ordered pairs with disjoint elements. See also snsn0non 6482. (Contributed by NM, 1-Jun-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (On ∩ (V × V)) = ∅
Theorem	onnev 6484	The class of ordinal numbers is not equal to the universe. (Contributed by NM, 16-Jun-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2013.) (Proof shortened by Wolf Lammen, 27-May-2024.)
⊢ On ≠ V
2.3.15  Definite description binder (inverted iota)
Syntax	cio 6485	Extend class notation with Russell's definition description binder (inverted iota).
class (℩𝑥𝜑)
Theorem	iotajust 6486*	Soundness justification theorem for df-iota 6487. (Contributed by Andrew Salmon, 29-Jun-2011.)
⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
Definition	df-iota 6487*	Define Russell's definition description binder, which can be read as "the unique 𝑥 such that 𝜑", where 𝜑 ordinarily contains 𝑥 as a free variable. Our definition is meaningful only when there is exactly one 𝑥 such that 𝜑 is true (see iotaval 6505); otherwise, it evaluates to the empty set (see iotanul 6511). Russell used the inverted iota symbol ℩ to represent the binder. Sometimes proofs need to expand an iota-based definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use riotacl2 7385 (or iotacl 6517 for unbounded iota), as demonstrated in the proof of supub 9435. This can be easier than applying riotasbc 7387 or a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
Theorem	dfiota2 6488*	Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)}
Theorem	nfiota1 6489	Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥(℩𝑥𝜑)
Theorem	nfiotadw 6490*	Deduction version of nfiotaw 6491. Version of nfiotad 6492 with a disjoint variable condition, which does not require ax-13 2402. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2402. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓))
Theorem	nfiotaw 6491*	Bound-variable hypothesis builder for the ℩ class. Version of nfiota 6493 with a disjoint variable condition, which does not require ax-13 2402. (Contributed by NM, 23-Aug-2011.) Avoid ax-13 2402. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥(℩𝑦𝜑)
Theorem	nfiotad 6492	Deduction version of nfiota 6493. Usage of this theorem is discouraged because it depends on ax-13 2402. Use the weaker nfiotadw 6490 when possible. (Contributed by NM, 18-Feb-2013.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓))
Theorem	nfiota 6493	Bound-variable hypothesis builder for the ℩ class. Usage of this theorem is discouraged because it depends on ax-13 2402. Use the weaker nfiotaw 6491 when possible. (Contributed by NM, 23-Aug-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥(℩𝑦𝜑)
Theorem	cbviotaw 6494*	Change bound variables in a description binder. Version of cbviota 6496 with a disjoint variable condition, which does not require ax-13 2402. (Contributed by Andrew Salmon, 1-Aug-2011.) Avoid ax-13 2402. (Revised by GG, 26-Jan-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviotavw 6495*	Change bound variables in a description binder. Version of cbviotav 6497 with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviota 6496	Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2402. Use the weaker cbviotaw 6494 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviotav 6497*	Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2402. Use the weaker cbviotavw 6495 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	sb8iota 6498	Variable substitution in description binder. Compare sb8eu 2626. Usage of this theorem is discouraged because it depends on ax-13 2402. (Contributed by NM, 18-Mar-2013.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑)
Theorem	iotaeq 6499	Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 2402. (Contributed by Andrew Salmon, 30-Jun-2011.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (℩𝑥𝜑) = (℩𝑦𝜑))
Theorem	iotabi 6500	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))