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	nfiotad 6501	Deduction version of nfiota 6502. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfiotadw 6499 when possible. (Contributed by NM, 18-Feb-2013.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(℩𝑦𝜓))
Theorem	nfiota 6502	Bound-variable hypothesis builder for the ℩ class. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfiotaw 6500 when possible. (Contributed by NM, 23-Aug-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥(℩𝑦𝜑)
Theorem	cbviotaw 6503*	Change bound variables in a description binder. Version of cbviota 6506 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Andrew Salmon, 1-Aug-2011.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviotavw 6504*	Change bound variables in a description binder. Version of cbviotav 6507 with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by Gino Giotto, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviotavwOLD 6505*	Obsolete version of cbviotavw 6504 as of 30-Sep-2024. (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by Gino Giotto, 26-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviota 6506	Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbviotaw 6503 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	cbviotav 6507*	Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbviotavw 6504 when possible. (Contributed by Andrew Salmon, 1-Aug-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)
Theorem	sb8iota 6508	Variable substitution in description binder. Compare sb8eu 2595. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 18-Mar-2013.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑)
Theorem	iotaeq 6509	Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by Andrew Salmon, 30-Jun-2011.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (℩𝑥𝜑) = (℩𝑦𝜑))
Theorem	iotabi 6510	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
Theorem	uniabio 6511*	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 6512*	Version of iotaval 6515 using df-iota 6496 instead of dfiota2 6497. (Contributed by SN, 6-Nov-2024.)
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
Theorem	iotauni2 6513*	Version of iotauni 6519 using df-iota 6496 instead of dfiota2 6497. (Contributed by SN, 6-Nov-2024.)
⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑})
Theorem	iotanul2 6514*	Version of iotanul 6522 using df-iota 6496 instead of dfiota2 6497. (Contributed by SN, 6-Nov-2024.)
⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
Theorem	iotaval 6515*	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 2138, ax-11 2155, ax-12 2172. (Revised by SN, 23-Nov-2024.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦)
Theorem	iotassuni 6516	The ℩ class is a subset of the union of all elements satisfying 𝜑. (Contributed by Mario Carneiro, 24-Dec-2016.) Remove dependency on ax-10 2138, ax-11 2155, ax-12 2172. (Revised by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) ⊆ ∪ {𝑥 ∣ 𝜑}
Theorem	iotaex 6517	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 2138, ax-11 2155, ax-12 2172. (Revised by SN, 6-Nov-2024.)
⊢ (℩𝑥𝜑) ∈ V
Theorem	iotavalOLD 6518*	Obsolete version of iotaval 6515 as of 23-Dec-2024. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦)
Theorem	iotauni 6519	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∪ {𝑥 ∣ 𝜑})
Theorem	iotaint 6520	Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) = ∩ {𝑥 ∣ 𝜑})
Theorem	iota1 6521	Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥𝜑 → (𝜑 ↔ (℩𝑥𝜑) = 𝑥))
Theorem	iotanul 6522	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	iotassuniOLD 6523	Obsolete version of iotassuni 6516 as of 23-Dec-2024. (Contributed by Mario Carneiro, 24-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (℩𝑥𝜑) ⊆ ∪ {𝑥 ∣ 𝜑}
Theorem	iotaexOLD 6524	Obsolete version of iotaex 6517 as of 23-Dec-2024. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (℩𝑥𝜑) ∈ V
Theorem	iota4 6525	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → [(℩𝑥𝜑) / 𝑥]𝜑)
Theorem	iota4an 6526	Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥(𝜑 ∧ 𝜓) → [(℩𝑥(𝜑 ∧ 𝜓)) / 𝑥]𝜑)
Theorem	iota5 6527*	A method for computing iota. (Contributed by NM, 17-Sep-2013.)
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴)
Theorem	iotabidv 6528*	Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))
Theorem	iotabii 6529	Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (℩𝑥𝜑) = (℩𝑥𝜓)
Theorem	iotacl 6530	Membership law for descriptions. This can be useful for expanding an unbounded iota-based definition (see df-iota 6496). If you have a bounded iota-based definition, riotacl2 7382 may be useful. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ {𝑥 ∣ 𝜑})
Theorem	iota2df 6531	A condition that allows to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → ∃!𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵))
Theorem	iota2d 6532*	A condition that allows to represent "the unique element such that 𝜑 " with a class expression 𝐴. (Contributed by NM, 30-Dec-2014.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → ∃!𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ↔ (℩𝑥𝜓) = 𝐵))
Theorem	iota2 6533*	The unique element such that 𝜑. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴))
Theorem	iotan0 6534*	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 6535	A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} = {(℩𝑥𝜑)})
Theorem	dfiota4 6536	The ℩ operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.) (Proof shortened by JJ, 28-Oct-2021.)
⊢ (℩𝑥𝜑) = if(∃!𝑥𝜑, ∪ {𝑥 ∣ 𝜑}, ∅)
Theorem	csbiota 6537*	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 6538	Extend the definition of a wff to include the function predicate. (Read: 𝐴 is a function.)
wff Fun 𝐴
Syntax	wfn 6539	Extend the definition of a wff to include the function predicate with a domain. (Read: 𝐴 is a function on 𝐵.)
wff 𝐴 Fn 𝐵
Syntax	wf 6540	Extend the definition of a wff to include the function predicate with domain and codomain. (Read: 𝐹 maps 𝐴 into 𝐵.)
wff 𝐹:𝐴⟶𝐵
Syntax	wf1 6541	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 6542	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 6543	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 6544	Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴", or "𝐹 of 𝐴".
class (𝐹‘𝐴)
Syntax	wiso 6545	Extend the definition of a wff to include the isomorphism property. Read: "𝐻 is an 𝑅, 𝑆 isomorphism of 𝐴 onto 𝐵".
wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
Definition	df-fun 6546	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 16014). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 5232 with the maps-to notation (see df-mpt 5233 and df-mpo 7414). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 6547), a function with a given domain and codomain (df-f 6548), a one-to-one function (df-f1 6549), an onto function (df-fo 6550), or a one-to-one onto function (df-f1o 6551). For alternate definitions, see dffun2 6554, dffun3 6558, dffun4 6560, dffun5 6561, dffun6 6557, dffun7 6576, dffun8 6577, and dffun9 6578. (Contributed by NM, 1-Aug-1994.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
Definition	df-fn 6547	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6720, dffn3 6731, dffn4 6812, and dffn5 6951. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Definition	df-f 6548	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 7101, dff3 7102, and dff4 7103. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
Definition	df-f1 6549	Define a one-to-one function. For equivalent definitions see dff12 6787 and dff13 7254. 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 18037. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
Definition	df-fo 6550	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 6810, dffo3 7104, dffo4 7105, and dffo5 7106. 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 18038. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Definition	df-f1o 6551	Define a one-to-one onto function. For equivalent definitions see dff1o2 6839, dff1o3 6840, dff1o4 6842, and dff1o5 6843. 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 18041. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7321, 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 8949. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
Definition	df-fv 6552*	Define the value of a function, (𝐹‘𝐴), also known as function application. For example, (cos‘0) = 1 (we prove this in cos0 16093 after we define cosine in df-cos 16014). Typically, function 𝐹 is defined using maps-to notation (see df-mpt 5233 and df-mpo 7414), but this is not required. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘3) = 9 (ex-fv 29696). Note that df-ov 7412 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 6927 and fvprc 6884). 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 6987, dffv3 6888, fv2 6887, and fv3 6910 (the latter two previously required 𝐴 to be a set.) Restricted equivalents that require 𝐹 to be a function are shown in funfv 6979 and funfv2 6980. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 6948. (Contributed by NM, 1-Aug-1994.) Revised to use ℩. Original version is now Theorem dffv4 6889. (Revised by Scott Fenton, 6-Oct-2017.)
⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
Definition	df-isom 6553*	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-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
Theorem	dffun2 6554*	Alternate definition of a function. (Contributed by NM, 29-Dec-1996.) Avoid ax-10 2138, ax-12 2172. (Revised by SN, 19-Dec-2024.) Avoid ax-11 2155. (Revised by BTernaryTau, 29-Dec-2024.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))
Theorem	dffun2OLD 6555*	Obsolete version of dffun2 6554 as of 29-Dec-2024. (Contributed by NM, 29-Dec-1996.) Avoid ax-10 2138, ax-12 2172. (Revised by SN, 19-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))
Theorem	dffun2OLDOLD 6556*	Obsolete version of dffun2 6554 as of 11-Dec-2024. (Contributed by NM, 29-Dec-1996.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))
Theorem	dffun6 6557*	Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) Avoid ax-10 2138, ax-12 2172. (Revised by SN, 19-Dec-2024.)
⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))
Theorem	dffun3 6558*	Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Proof shortened by SN, 19-Dec-2024.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(𝑥𝐴𝑦 → 𝑦 = 𝑧)))
Theorem	dffun3OLD 6559*	Obsolete version of dffun3 6558 as of 19-Dec-2024. Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(𝑥𝐴𝑦 → 𝑦 = 𝑧)))
Theorem	dffun4 6560*	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 29-Dec-1996.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)))
Theorem	dffun5 6561*	Alternate definition of function. (Contributed by NM, 29-Dec-1996.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑦 = 𝑧)))
Theorem	dffun6f 6562*	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	dffun6OLD 6563*	Obsolete version of dffun6 6557 as of 19-Dec-2024. (Contributed by NM, 9-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))
Theorem	funmo 6564*	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	funmoOLD 6565*	Obsolete version of funmo 6564 as of 19-Dec-2024. (Contributed by NM, 24-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fun 𝐹 → ∃*𝑦 𝐴𝐹𝑦)
Theorem	funrel 6566	A function is a relation. (Contributed by NM, 1-Aug-1994.)
⊢ (Fun 𝐴 → Rel 𝐴)
Theorem	0nelfun 6567	A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021.)
⊢ (Fun 𝑅 → ∅ ∉ 𝑅)
Theorem	funss 6568	Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
Theorem	funeq 6569	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
Theorem	funeqi 6570	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Fun 𝐴 ↔ Fun 𝐵)
Theorem	funeqd 6571	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))
Theorem	nffun 6572	Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥Fun 𝐹
Theorem	sbcfung 6573	Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Fun 𝐹 ↔ Fun ⦋𝐴 / 𝑥⦌𝐹))
Theorem	funeu 6574*	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 6575*	There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.)
⊢ ((Fun 𝐹 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐹) → ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹)
Theorem	dffun7 6576*	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 6577 shows that it does not matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
Theorem	dffun8 6577*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 6576. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦))
Theorem	dffun9 6578*	Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 ∈ ran 𝐴 𝑥𝐴𝑦))
Theorem	funfn 6579	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 6580	A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → Fun 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 Fn dom 𝐴)
Theorem	funi 6581	The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. See also idfn 6679. (Contributed by NM, 30-Apr-1998.)
⊢ Fun I
Theorem	nfunv 6582	The universal class is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
⊢ ¬ Fun V
Theorem	funopg 6583	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 6600, as relsnopg 5804 is to relop 5851. (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun ⟨𝐴, 𝐵⟩) → 𝐴 = 𝐵)
Theorem	funopab 6584*	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 6585*	A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐴}
Theorem	funopab4 6586*	A class of ordered pairs of values in the form used by df-mpt 5233 is a function. (Contributed by NM, 17-Feb-2013.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝑦 = 𝐴)}
Theorem	funmpt 6587	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	funmpt2 6588	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 6589	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 (𝐹 ∘ 𝐺))
Theorem	funresfunco 6590	Composition of two functions, generalization of funco 6589. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
⊢ ((Fun (𝐹 ↾ ran 𝐺) ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺))
Theorem	funres 6591	A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.)
⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))
Theorem	funresd 6592	A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → Fun (𝐹 ↾ 𝐴))
Theorem	funssres 6593	The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺)
Theorem	fun2ssres 6594	Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ⊆ dom 𝐺) → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴))
Theorem	funun 6595	The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by NM, 12-Aug-1994.)
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺))
Theorem	fununmo 6596*	If the union of classes is a function, there is at most one element in relation to an arbitrary element regarding one of these classes. (Contributed by AV, 18-Jul-2019.)
⊢ (Fun (𝐹 ∪ 𝐺) → ∃*𝑦 𝑥𝐹𝑦)
Theorem	fununfun 6597	If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019.)
⊢ (Fun (𝐹 ∪ 𝐺) → (Fun 𝐹 ∧ Fun 𝐺))
Theorem	fundif 6598	A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021.)
⊢ (Fun 𝐹 → Fun (𝐹 ∖ 𝐴))
Theorem	funcnvsn 6599	The converse singleton of an ordered pair is a function. This is equivalent to funsn 6602 via cnvsn 6226, but stating it this way allows to skip the sethood assumptions on 𝐴 and 𝐵. (Contributed by NM, 30-Apr-2015.)
⊢ Fun ◡{⟨𝐴, 𝐵⟩}
Theorem	funsng 6600	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 28-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {⟨𝐴, 𝐵⟩})