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	sucid 6401	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 6402	No successor is empty. (Contributed by NM, 3-Apr-1995.)
⊢ suc 𝐴 ≠ ∅
Theorem	eqelsuc 6403	A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵)
Theorem	iunsuc 6404*	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 6405	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 6406	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 6407	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 6408	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 6409	A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵))
Theorem	ordsssuc2 6410	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 6411	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 6412	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 6413	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 6414	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 6415	Ordinal derived from its successor. (Contributed by NM, 20-May-1998.)
⊢ (Ord 𝐴 → 𝐴 = (suc 𝐴 ∖ {𝐴}))
Theorem	orduniss 6416	An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.)
⊢ (Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴)
Theorem	ordtri2or 6417	A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	ordtri2or2 6418	A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	ordtri2or3 6419	A consequence of total ordering for ordinal classes. Similar to ordtri2or2 6418. (Contributed by David Moews, 1-May-2017.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = (𝐴 ∩ 𝐵) ∨ 𝐵 = (𝐴 ∩ 𝐵)))
Theorem	ordelinel 6420	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 6421	Property of a subclass of the maximum (i.e. union) of two ordinals. (Contributed by NM, 28-Nov-2003.)
⊢ ((Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶)))
Theorem	ordequn 6422	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 6423	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 6424	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 6425	A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003.)
⊢ ((𝐴 ⊆ On ∧ Ord 𝐵) → (∪ 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵))
Theorem	suc11 6426	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 6427	The union of two ordinals is an ordinal. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On)
Theorem	ontr 6428	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 6429	An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) Generalize from onunisuci 6438. (Revised by BJ, 28-Dec-2024.)
⊢ (𝐴 ∈ On → ∪ suc 𝐴 = 𝐴)
Theorem	onordi 6430	An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ Ord 𝐴
Theorem	onirri 6431	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 6432	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 6433	A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)
Theorem	onssneli 6434	An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 ⊆ 𝐵 → ¬ 𝐵 ∈ 𝐴)
Theorem	onssnel2i 6435	An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ⊆ 𝐴 → ¬ 𝐴 ∈ 𝐵)
Theorem	onelini 6436	An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴))
Theorem	oneluni 6437	An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴)
Theorem	onunisuci 6438	An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ ∪ suc 𝐴 = 𝐴
Theorem	onsseli 6439	Subset is equivalent to membership or equality for ordinal numbers. (Contributed by NM, 15-Sep-1995.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	onun2i 6440	The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    ⇒   ⊢ (𝐴 ∪ 𝐵) ∈ On
Theorem	unizlim 6441	An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴)))
Theorem	on0eqel 6442	An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004.)
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈ 𝐴))
Theorem	snsn0non 6443	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 7812). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 6444. (Contributed by NM, 21-May-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ ¬ {{∅}} ∈ On
Theorem	onxpdisj 6444	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 6443. (Contributed by NM, 1-Jun-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (On ∩ (V × V)) = ∅
Theorem	onnev 6445	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 6446	Extend class notation with Russell's definition description binder (inverted iota).
class (℩𝑥𝜑)
Theorem	iotajust 6447*	Soundness justification theorem for df-iota 6448. (Contributed by Andrew Salmon, 29-Jun-2011.)
⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
Definition	df-iota 6448*	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 6466); otherwise, it evaluates to the empty set (see iotanul 6472). 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 7331 (or iotacl 6478 for unbounded iota), as demonstrated in the proof of supub 9362. This can be easier than applying riotasbc 7333 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 6449*	Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)}
Theorem	nfiota1 6450	Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥(℩𝑥𝜑)
Theorem	nfiotadw 6451*	Deduction version of nfiotaw 6452. Version of nfiotad 6453 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2376. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓))
Theorem	nfiotaw 6452*	Bound-variable hypothesis builder for the ℩ class. Version of nfiota 6454 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by NM, 23-Aug-2011.) Avoid ax-13 2376. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥(℩𝑦𝜑)
Theorem	nfiotad 6453	Deduction version of nfiota 6454. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker nfiotadw 6451 when possible. (Contributed by NM, 18-Feb-2013.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓))
Theorem	nfiota 6454	Bound-variable hypothesis builder for the ℩ class. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker nfiotaw 6452 when possible. (Contributed by NM, 23-Aug-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥(℩𝑦𝜑)
Theorem	cbviotaw 6455*	Change bound variables in a description binder. Version of cbviota 6457 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by Andrew Salmon, 1-Aug-2011.) Avoid ax-13 2376. (Revised by GG, 26-Jan-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviotavw 6456*	Change bound variables in a description binder. Version of cbviotav 6458 with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviota 6457	Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker cbviotaw 6455 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviotav 6458*	Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker cbviotavw 6456 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	sb8iota 6459	Variable substitution in description binder. Compare sb8eu 2600. Usage of this theorem is discouraged because it depends on ax-13 2376. (Contributed by NM, 18-Mar-2013.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑)
Theorem	iotaeq 6460	Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 2376. (Contributed by Andrew Salmon, 30-Jun-2011.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (℩𝑥𝜑) = (℩𝑦𝜑))
Theorem	iotabi 6461	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
Theorem	uniabio 6462*	Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∪ {𝑥 ∣ 𝜑} = 𝑦)
Theorem	iotaval2 6463*	Version of iotaval 6466 using df-iota 6448 instead of dfiota2 6449. (Contributed by SN, 6-Nov-2024.)
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
Theorem	iotauni2 6464*	Version of iotauni 6469 using df-iota 6448 instead of dfiota2 6449. (Contributed by SN, 6-Nov-2024.)
⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑})
Theorem	iotanul2 6465*	Version of iotanul 6472 using df-iota 6448 instead of dfiota2 6449. (Contributed by SN, 6-Nov-2024.)
⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
Theorem	iotaval 6466*	Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) Remove dependency on ax-10 2146, ax-11 2162, ax-12 2184. (Revised by SN, 23-Nov-2024.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦)
Theorem	iotassuni 6467	The ℩ class is a subset of the union of all elements satisfying 𝜑. (Contributed by Mario Carneiro, 24-Dec-2016.) Remove dependency on ax-10 2146, ax-11 2162, ax-12 2184. (Revised by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) ⊆ ∪ {𝑥 ∣ 𝜑}
Theorem	iotaex 6468	Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the ℩ class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.) Remove dependency on ax-10 2146, ax-11 2162, ax-12 2184. (Revised by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) ∈ V
Theorem	iotauni 6469	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑})
Theorem	iotaint 6470	Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∩ {𝑥 ∣ 𝜑})
Theorem	iota1 6471	Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥𝜑 → (𝜑 ↔ (℩𝑥𝜑) = 𝑥))
Theorem	iotanul 6472	Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one 𝑥 that satisfies 𝜑. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (¬ ∃!𝑥𝜑 → (℩𝑥𝜑) = ∅)
Theorem	iota4 6473	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → [(℩𝑥𝜑) / 𝑥]𝜑)
Theorem	iota4an 6474	Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥(𝜑 ∧ 𝜓) → [(℩𝑥(𝜑 ∧ 𝜓)) / 𝑥]𝜑)
Theorem	iota5 6475*	A method for computing iota. (Contributed by NM, 17-Sep-2013.)
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴)
Theorem	iotabidv 6476*	Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))
Theorem	iotabii 6477	Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑥𝜓)
Theorem	iotacl 6478	Membership law for descriptions. This can be useful for expanding an unbounded iota-based definition (see df-iota 6448). If you have a bounded iota-based definition, riotacl2 7331 may be useful. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ {𝑥 ∣ 𝜑})
Theorem	iota2df 6479	A condition that allows to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → ∃!𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵))
Theorem	iota2d 6480*	A condition that allows to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → ∃!𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵))
Theorem	iota2 6481*	The unique element such that 𝜑. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴))
Theorem	iotan0 6482*	Representation of "the unique element such that 𝜑 " with a class expression 𝐴 which is not the empty set (that means that "the unique element such that 𝜑 " exists). (Contributed by AV, 30-Jan-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = (℩𝑥𝜑)) → 𝜓)
Theorem	sniota 6483	A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} = {(℩𝑥𝜑)})
Theorem	dfiota4 6484	The ℩ operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.) (Proof shortened by JJ, 28-Oct-2021.)
⊢ (℩𝑥𝜑) = if(∃!𝑥𝜑, ∪ {𝑥 ∣ 𝜑}, ∅)
Theorem	csbiota 6485*	Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.) (Revised by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(℩𝑦𝜑) = (℩𝑦[𝐴 / 𝑥]𝜑)
2.3.16  Functions
Syntax	wfun 6486	Extend the definition of a wff to include the function predicate. (Read: 𝐴 is a function.)
wff Fun 𝐴
Syntax	wfn 6487	Extend the definition of a wff to include the function predicate with a domain. (Read: 𝐴 is a function on 𝐵.)
wff 𝐴 Fn 𝐵
Syntax	wf 6488	Extend the definition of a wff to include the function predicate with domain and codomain. (Read: 𝐹 maps 𝐴 into 𝐵.)
wff 𝐹:𝐴⟶𝐵
Syntax	wf1 6489	Extend the definition of a wff to include one-to-one functions. (Read: 𝐹 maps 𝐴 one-to-one into 𝐵.) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27.
wff 𝐹:𝐴–1-1→𝐵
Syntax	wfo 6490	Extend the definition of a wff to include onto functions. (Read: 𝐹 maps 𝐴 onto 𝐵.) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27.
wff 𝐹:𝐴–onto→𝐵
Syntax	wf1o 6491	Extend the definition of a wff to include one-to-one onto functions. (Read: 𝐹 maps 𝐴 one-to-one onto 𝐵.) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27.
wff 𝐹:𝐴–1-1-onto→𝐵
Syntax	cfv 6492	Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴", or "𝐹 of 𝐴".
class (𝐹‘𝐴)
Syntax	wiso 6493	Extend the definition of a wff to include the isomorphism property. Read: "𝐻 is an 𝑅, 𝑆 isomorphism of 𝐴 onto 𝐵".
wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
Definition	df-fun 6494	Define predicate that determines if some class 𝐴 is a function. Definition 10.1 of [Quine] p. 65. For example, the expression Fun cos is true once we define cosine (df-cos 15993). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 5179 with the maps-to notation (see df-mpt 5180 and df-mpo 7363). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 6495), a function with a given domain and codomain (df-f 6496), a one-to-one function (df-f1 6497), an onto function (df-fo 6498), or a one-to-one onto function (df-f1o 6499). For alternate definitions, see dffun2 6502, dffun3 6504, dffun4 6505, dffun5 6506, dffun6 6503, dffun7 6519, dffun8 6520, and dffun9 6521. (Contributed by NM, 1-Aug-1994.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
Definition	df-fn 6495	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6664, dffn3 6674, dffn4 6752, and dffn5 6892. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Definition	df-f 6496	Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. 𝐹:𝐴⟶𝐵 can be read as "𝐹 is a function from 𝐴 to 𝐵". For alternate definitions, see dff2 7044, dff3 7045, and dff4 7046. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
Definition	df-f1 6497	Define a one-to-one function. For equivalent definitions see dff12 6729 and dff13 7200. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). A one-to-one function is also called an "injection" or an "injective function", 𝐹:𝐴–1-1→𝐵 can be read as "𝐹 is an injection from 𝐴 into 𝐵". Injections are precisely the monomorphisms in the category SetCat of sets and set functions, see setcmon 18011. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
Definition	df-fo 6498	Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 6750, dffo3 7047, dffo4 7048, and dffo5 7049. An onto function is also called a "surjection" or a "surjective function", 𝐹:𝐴–onto→𝐵 can be read as "𝐹 is a surjection from 𝐴 onto 𝐵". Surjections are precisely the epimorphisms in the category SetCat of sets and set functions, see setcepi 18012. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Definition	df-f1o 6499	Define a one-to-one onto function. For equivalent definitions see dff1o2 6779, dff1o3 6780, dff1o4 6782, and dff1o5 6783. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). A one-to-one onto function is also called a "bijection" or a "bijective function", 𝐹:𝐴–1-1-onto→𝐵 can be read as "𝐹 is a bijection between 𝐴 and 𝐵". Bijections are precisely the isomorphisms in the category SetCat of sets and set functions, see setciso 18015. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7270, two sets are isomorphic iff there is an isomorphism Isom regarding the identity relation. In this case, the two sets are also "equinumerous", see bren 8893. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
Definition	df-fv 6500*	Define the value of a function, (𝐹‘𝐴), also known as function application. For example, (cos‘0) = 1 (we prove this in cos0 16075 after we define cosine in df-cos 15993). Typically, function 𝐹 is defined using maps-to notation (see df-mpt 5180 and df-mpo 7363), but this is not required. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘3) = 9 (ex-fv 30518). Note that df-ov 7361 will define two-argument functions using ordered pairs as (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩). This particular definition is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful (as shown by ndmfv 6866 and fvprc 6826). The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It means the same thing as the more familiar 𝐹(𝐴) notation for a function's value at 𝐴, i.e., "𝐹 of 𝐴", but without context-dependent notational ambiguity. Alternate definitions are dffv2 6929, dffv3 6830, fv2 6829, and fv3 6852 (the latter two previously required 𝐴 to be a set.) Restricted equivalents that require 𝐹 to be a function are shown in funfv 6921 and funfv2 6922. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 6888. (Contributed by NM, 1-Aug-1994.) Revised to use ℩. Original version is now Theorem dffv4 6831. (Revised by Scott Fenton, 6-Oct-2017.)
⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)