P. 66 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6501-6600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oneluni 6501	An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴)
Theorem	onunisuci 6502	An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ ∪ suc 𝐴 = 𝐴
Theorem	onsseli 6503	Subset is equivalent to membership or equality for ordinal numbers. (Contributed by NM, 15-Sep-1995.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    ⇒   ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	onun2i 6504	The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    ⇒   ⊢ (𝐴 ∪ 𝐵) ∈ On
Theorem	unizlim 6505	An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.)
⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴)))
Theorem	on0eqel 6506	An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004.)
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈ 𝐴))
Theorem	snsn0non 6507	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 7905). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 6508. (Contributed by NM, 21-May-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ ¬ {{∅}} ∈ On
Theorem	onxpdisj 6508	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 6507. (Contributed by NM, 1-Jun-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (On ∩ (V × V)) = ∅
Theorem	onnev 6509	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 6510	Extend class notation with Russell's definition description binder (inverted iota).
class (℩𝑥𝜑)
Theorem	iotajust 6511*	Soundness justification theorem for df-iota 6512. (Contributed by Andrew Salmon, 29-Jun-2011.)
⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
Definition	df-iota 6512*	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 6530); otherwise, it evaluates to the empty set (see iotanul 6537). 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 7416 (or iotacl 6543 for unbounded iota), as demonstrated in the proof of supub 9478. This can be easier than applying riotasbc 7418 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 6513*	Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)}
Theorem	nfiota1 6514	Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥(℩𝑥𝜑)
Theorem	nfiotadw 6515*	Deduction version of nfiotaw 6516. Version of nfiotad 6517 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2404. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓))
Theorem	nfiotaw 6516*	Bound-variable hypothesis builder for the ℩ class. Version of nfiota 6518 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 23-Aug-2011.) Avoid ax-13 2404. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥(℩𝑦𝜑)
Theorem	nfiotad 6517	Deduction version of nfiota 6518. Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker nfiotadw 6515 when possible. (Contributed by NM, 18-Feb-2013.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓))
Theorem	nfiota 6518	Bound-variable hypothesis builder for the ℩ class. Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker nfiotaw 6516 when possible. (Contributed by NM, 23-Aug-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥(℩𝑦𝜑)
Theorem	cbviotaw 6519*	Change bound variables in a description binder. Version of cbviota 6521 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by Andrew Salmon, 1-Aug-2011.) Avoid ax-13 2404. (Revised by GG, 26-Jan-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviotavw 6520*	Change bound variables in a description binder. Version of cbviotav 6522 with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviota 6521	Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker cbviotaw 6519 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviotav 6522*	Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker cbviotavw 6520 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	sb8iota 6523	Variable substitution in description binder. Compare sb8eu 2628. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 18-Mar-2013.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑)
Theorem	iotaeq 6524	Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by Andrew Salmon, 30-Jun-2011.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (℩𝑥𝜑) = (℩𝑦𝜑))
Theorem	iotabi 6525	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
Theorem	uniabio 6526*	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 6527*	Version of iotaval 6530 using df-iota 6512 instead of dfiota2 6513. (Contributed by SN, 6-Nov-2024.)
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
Theorem	iotauni2 6528*	Version of iotauni 6534 using df-iota 6512 instead of dfiota2 6513. (Contributed by SN, 6-Nov-2024.)
⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑})
Theorem	iotanul2 6529*	Version of iotanul 6537 using df-iota 6512 instead of dfiota2 6513. (Contributed by SN, 6-Nov-2024.)
⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
Theorem	iotaval 6530*	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 2180, ax-11 2197, ax-12 2216. (Revised by SN, 23-Nov-2024.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦)
Theorem	iotain 6531	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} = (℩𝑥𝜑))
Theorem	iotassuni 6532	The ℩ class is a subset of the union of all elements satisfying 𝜑. (Contributed by Mario Carneiro, 24-Dec-2016.) Remove dependency on ax-10 2180, ax-11 2197, ax-12 2216. (Revised by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) ⊆ ∪ {𝑥 ∣ 𝜑}
Theorem	iotaex 6533	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 2180, ax-11 2197, ax-12 2216. (Revised by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) ∈ V
Theorem	iotauni 6534	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑})
Theorem	iotaint 6535	Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∩ {𝑥 ∣ 𝜑})
Theorem	iota1 6536	Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥𝜑 → (𝜑 ↔ (℩𝑥𝜑) = 𝑥))
Theorem	iotanul 6537	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 6538	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → [(℩𝑥𝜑) / 𝑥]𝜑)
Theorem	iota4an 6539	Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥(𝜑 ∧ 𝜓) → [(℩𝑥(𝜑 ∧ 𝜓)) / 𝑥]𝜑)
Theorem	iota5 6540*	A method for computing iota. (Contributed by NM, 17-Sep-2013.)
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴)
Theorem	iotabidv 6541*	Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))
Theorem	iotabii 6542	Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑥𝜓)
Theorem	iotacl 6543	Membership law for descriptions. This can be useful for expanding an unbounded iota-based definition (see df-iota 6512). If you have a bounded iota-based definition, riotacl2 7416 may be useful. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ {𝑥 ∣ 𝜑})
Theorem	iota2df 6544	A condition that allows to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → ∃!𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵))
Theorem	iota2d 6545*	A condition that allows to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → ∃!𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵))
Theorem	iota2 6546*	The unique element such that 𝜑. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴))
Theorem	iotan0 6547*	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.) Remove sethood antecedent. (Revised by Eric Schmidt, 17-Oct-2026.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 = (℩𝑥𝜑)) → 𝜓)
Theorem	iotan0OLD 6548*	Obsolete version of iotan0 6547 as of 17-Oct-2026. (Contributed by AV, 30-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = (℩𝑥𝜑)) → 𝜓)
Theorem	sniota 6549	A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} = {(℩𝑥𝜑)})
Theorem	dfiota4 6550	The ℩ operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.) (Proof shortened by JJ, 28-Oct-2021.)
⊢ (℩𝑥𝜑) = if(∃!𝑥𝜑, ∪ {𝑥 ∣ 𝜑}, ∅)
Theorem	csbiota 6551*	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 6552	Extend the definition of a wff to include the function predicate. (Read: 𝐴 is a function.)
wff Fun 𝐴
Syntax	wfn 6553	Extend the definition of a wff to include the function predicate with a domain. (Read: 𝐴 is a function on 𝐵.)
wff 𝐴 Fn 𝐵
Syntax	wf 6554	Extend the definition of a wff to include the function predicate with domain and codomain. (Read: 𝐹 maps 𝐴 into 𝐵.)
wff 𝐹:𝐴⟶𝐵
Syntax	wf1 6555	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 6556	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 6557	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-1onto𝐵
Syntax	cfv 6558	Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴", or "𝐹 of 𝐴".
class (𝐹‘𝐴)
Syntax	wiso 6559	Extend the definition of a wff to include the isomorphism property. Read: "𝐻 is an 𝑅, 𝑆 isomorphism of 𝐴 onto 𝐵".
wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
Definition	df-fun 6560	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 16265). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 5189 with the maps-to notation (see df-mpt 5190 and df-mpo 7448). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 6561), a function with a given domain and codomain (df-f 6562), a one-to-one function (df-f1 6563), an onto function (df-fo 6564), or a one-to-one onto function (df-f1o 6565). For alternate definitions, see dffun2 6568, dffun3 6570, dffun4 6571, dffun5 6572, dffun6 6569, dffun7 6587, dffun8 6588, and dffun9 6589. (Contributed by NM, 1-Aug-1994.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
Definition	df-fn 6561	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6733, dffn3 6744, dffn4 6824, and dffn5 6966. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Definition	df-f 6562	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 7123, dff3 7124, and dff4 7125. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
Definition	df-f1 6563	Define a one-to-one function. For equivalent definitions see dff12 6799 and dff13 7281. 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 18291. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴⟶1-1𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
Definition	df-fo 6564	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 6822, dffo3 7126, dffo4 7127, and dffo5 7128. 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 18292. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴⟶onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Definition	df-f1o 6565	Define a one-to-one onto function. For equivalent definitions see dff1o2 6852, dff1o3 6853, dff1o4 6855, and dff1o5 6856. 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-1onto𝐵 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 18295. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7355, 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 9011. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶1-1𝐵 ∧ 𝐹:𝐴⟶onto𝐵))
Definition	df-fv 6566*	Define the value of a function, (𝐹‘𝐴), also known as function application. For example, (cos‘0) = 1 (we prove this in cos0 16347 after we define cosine in df-cos 16265). Typically, function 𝐹 is defined using maps-to notation (see df-mpt 5190 and df-mpo 7448), but this is not required. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘3) = 9 (ex-fv 31074). Note that df-ov 7446 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 6940 and fvprc 6900). 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 7003, dffv3 6904, fv2 6903, and fv3 6926 (the latter two previously required 𝐴 to be a set.) Restricted equivalents that require 𝐹 to be a function are shown in funfv 6995 and funfv2 6996. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 6962. (Contributed by NM, 1-Aug-1994.) Revised to use ℩. Original version is now Theorem dffv4 6905. (Revised by Scott Fenton, 6-Oct-2017.)
⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
Definition	df-isom 6567*	Define the isomorphism predicate. We read this as "𝐻 is an 𝑅, 𝑆 isomorphism of 𝐴 onto 𝐵". Normally, 𝑅 and 𝑆 are ordering relations on 𝐴 and 𝐵 respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that 𝑅 and 𝑆 are subscripts. (Contributed by NM, 4-Mar-1997.)
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴⟶1-1onto𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
Theorem	dffun2 6568*	Alternate definition of a function. (Contributed by NM, 29-Dec-1996.) Avoid ax-10 2180, ax-12 2216. (Revised by SN, 19-Dec-2024.) Avoid ax-11 2197. (Revised by BTernaryTau, 29-Dec-2024.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))
Theorem	dffun6 6569*	Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) Avoid ax-10 2180, ax-12 2216. (Revised by SN, 19-Dec-2024.)
⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))
Theorem	dffun3 6570*	Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Proof shortened by SN, 19-Dec-2024.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(𝑥𝐴𝑦 → 𝑦 = 𝑧)))
Theorem	dffun4 6571*	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 29-Dec-1996.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)))
Theorem	dffun5 6572*	Alternate definition of function. (Contributed by NM, 29-Dec-1996.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑦 = 𝑧)))
Theorem	dffun6f 6573*	Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦))
Theorem	funmo 6574*	A function has at most one value for each argument. (Contributed by NM, 24-May-1998.) (Proof shortened by SN, 19-Dec-2024.)
⊢ (Fun 𝐹 → ∃*𝑦 𝐴𝐹𝑦)
Theorem	fununiq 6575	Functions are single-valued. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶))
Theorem	funrel 6576	A function is a relation. (Contributed by NM, 1-Aug-1994.)
⊢ (Fun 𝐴 → Rel 𝐴)
Theorem	0nelfun 6577	A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021.)
⊢ (Fun 𝑅 → ∅ ∉ 𝑅)
Theorem	funss 6578	Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
Theorem	funeq 6579	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
Theorem	funeqi 6580	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Fun 𝐴 ↔ Fun 𝐵)
Theorem	funeqd 6581	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))
Theorem	nffun 6582	Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥Fun 𝐹
Theorem	sbcfung 6583	Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) Shorten proof and remove dependency on ax-sep 5252 and ax-pr 5395. (Revised by Eric Schmidt, 12-Sep-2026.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Fun 𝐹 ↔ Fun ⦋𝐴 / 𝑥⦌𝐹))
Theorem	sbcfungOLD 6584	Obsolete version of sbcfung 6583 as of 12-Sep-2026. (Contributed by Alexander van der Vekens, 23-Jul-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Fun 𝐹 ↔ Fun ⦋𝐴 / 𝑥⦌𝐹))
Theorem	funeu 6585*	There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → ∃!𝑦 𝐴𝐹𝑦)
Theorem	funeu2 6586*	There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.)
⊢ ((Fun 𝐹 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐹) → ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹)
Theorem	dffun7 6587*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one". However, dffun8 6588 shows that it does not matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
Theorem	dffun8 6588*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 6587. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦))
Theorem	dffun9 6589*	Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 ∈ ran 𝐴 𝑥𝐴𝑦))
Theorem	funfn 6590	A class is a function if and only if it is a function on its domain. (Contributed by NM, 13-Aug-2004.)
⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
Theorem	funfnd 6591	A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → Fun 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 Fn dom 𝐴)
Theorem	funi 6592	The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. See also idfn 6689. (Contributed by NM, 30-Apr-1998.)
⊢ Fun I
Theorem	nfunv 6593	The universal class is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
⊢ ¬ Fun V
Theorem	funopg 6594	A Kuratowski ordered pair of sets is a function only if its components are equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng 6613, as relsnopg 5786 is to relop 5834. (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun ⟨𝐴, 𝐵⟩) → 𝐴 = 𝐵)
Theorem	funopab 6595*	A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995.)
⊢ (Fun {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∀𝑥∃*𝑦𝜑)
Theorem	funopabeq 6596*	A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐴}
Theorem	funopab4 6597*	A class of ordered pairs of values in the form used by df-mpt 5190 is a function. (Contributed by NM, 17-Feb-2013.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝑦 = 𝐴)}
Theorem	funmpt 6598	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	funmpt2 6599	Functionality of a class given by a maps-to notation. (Contributed by FL, 17-Feb-2008.) (Revised by Mario Carneiro, 31-May-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ Fun 𝐹
Theorem	funco 6600	The composition of two functions is a function. Exercise 29 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺))