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
Syntax	wiso 6501	Extend the definition of a wff to include the isomorphism property. Read: "𝐻 is an 𝑅, 𝑆 isomorphism of 𝐴 onto 𝐵".
wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
Definition	df-fun 6502	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 16005). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 5181 with the maps-to notation (see df-mpt 5182 and df-mpo 7373). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 6503), a function with a given domain and codomain (df-f 6504), a one-to-one function (df-f1 6505), an onto function (df-fo 6506), or a one-to-one onto function (df-f1o 6507). For alternate definitions, see dffun2 6510, dffun3 6512, dffun4 6513, dffun5 6514, dffun6 6511, dffun7 6527, dffun8 6528, and dffun9 6529. (Contributed by NM, 1-Aug-1994.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
Definition	df-fn 6503	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6672, dffn3 6682, dffn4 6760, and dffn5 6900. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
Definition	df-f 6504	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 7053, dff3 7054, and dff4 7055. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
Definition	df-f1 6505	Define a one-to-one function. For equivalent definitions see dff12 6737 and dff13 7210. 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 18023. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
Definition	df-fo 6506	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 6758, dffo3 7056, dffo4 7057, and dffo5 7058. 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 18024. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Definition	df-f1o 6507	Define a one-to-one onto function. For equivalent definitions see dff1o2 6787, dff1o3 6788, dff1o4 6790, and dff1o5 6791. 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 18027. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7280, 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 8905. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
Definition	df-fv 6508*	Define the value of a function, (𝐹‘𝐴), also known as function application. For example, (cos‘0) = 1 (we prove this in cos0 16087 after we define cosine in df-cos 16005). Typically, function 𝐹 is defined using maps-to notation (see df-mpt 5182 and df-mpo 7373), but this is not required. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘3) = 9 (ex-fv 30530). Note that df-ov 7371 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 6874 and fvprc 6834). 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 6937, dffv3 6838, fv2 6837, and fv3 6860 (the latter two previously required 𝐴 to be a set.) Restricted equivalents that require 𝐹 to be a function are shown in funfv 6929 and funfv2 6930. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 6896. (Contributed by NM, 1-Aug-1994.) Revised to use ℩. Original version is now Theorem dffv4 6839. (Revised by Scott Fenton, 6-Oct-2017.)
⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
Definition	df-isom 6509*	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 6510*	Alternate definition of a function. (Contributed by NM, 29-Dec-1996.) Avoid ax-10 2147, ax-12 2185. (Revised by SN, 19-Dec-2024.) Avoid ax-11 2163. (Revised by BTernaryTau, 29-Dec-2024.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))
Theorem	dffun6 6511*	Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) Avoid ax-10 2147, ax-12 2185. (Revised by SN, 19-Dec-2024.)
⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))
Theorem	dffun3 6512*	Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Proof shortened by SN, 19-Dec-2024.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(𝑥𝐴𝑦 → 𝑦 = 𝑧)))
Theorem	dffun4 6513*	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 29-Dec-1996.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)))
Theorem	dffun5 6514*	Alternate definition of function. (Contributed by NM, 29-Dec-1996.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃𝑧∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑦 = 𝑧)))
Theorem	dffun6f 6515*	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 6516*	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	funrel 6517	A function is a relation. (Contributed by NM, 1-Aug-1994.)
⊢ (Fun 𝐴 → Rel 𝐴)
Theorem	0nelfun 6518	A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021.)
⊢ (Fun 𝑅 → ∅ ∉ 𝑅)
Theorem	funss 6519	Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
Theorem	funeq 6520	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
Theorem	funeqi 6521	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Fun 𝐴 ↔ Fun 𝐵)
Theorem	funeqd 6522	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵))
Theorem	nffun 6523	Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥Fun 𝐹
Theorem	sbcfung 6524	Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Fun 𝐹 ↔ Fun ⦋𝐴 / 𝑥⦌𝐹))
Theorem	funeu 6525*	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 6526*	There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.)
⊢ ((Fun 𝐹 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐹) → ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹)
Theorem	dffun7 6527*	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 6528 shows that it does not matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
Theorem	dffun8 6528*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 6527. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦))
Theorem	dffun9 6529*	Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 ∈ ran 𝐴 𝑥𝐴𝑦))
Theorem	funfn 6530	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 6531	A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → Fun 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 Fn dom 𝐴)
Theorem	funi 6532	The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. See also idfn 6628. (Contributed by NM, 30-Apr-1998.)
⊢ Fun I
Theorem	nfunv 6533	The universal class is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
⊢ ¬ Fun V
Theorem	funopg 6534	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 6551, as relsnopg 5760 is to relop 5807. (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun ⟨𝐴, 𝐵⟩) → 𝐴 = 𝐵)
Theorem	funopab 6535*	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 6536*	A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐴}
Theorem	funopab4 6537*	A class of ordered pairs of values in the form used by df-mpt 5182 is a function. (Contributed by NM, 17-Feb-2013.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝑦 = 𝐴)}
Theorem	funmpt 6538	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	funmpt2 6539	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 6540	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 6541	Composition of two functions, generalization of funco 6540. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
⊢ ((Fun (𝐹 ↾ ran 𝐺) ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺))
Theorem	funres 6542	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 6543	A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → Fun (𝐹 ↾ 𝐴))
Theorem	funssres 6544	The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺)
Theorem	fun2ssres 6545	Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ⊆ dom 𝐺) → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴))
Theorem	funun 6546	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 6547*	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 6548	If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019.)
⊢ (Fun (𝐹 ∪ 𝐺) → (Fun 𝐹 ∧ Fun 𝐺))
Theorem	fundif 6549	A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021.)
⊢ (Fun 𝐹 → Fun (𝐹 ∖ 𝐴))
Theorem	funcnvsn 6550	The converse singleton of an ordered pair is a function. This is equivalent to funsn 6553 via cnvsn 6192, but stating it this way allows to skip the sethood assumptions on 𝐴 and 𝐵. (Contributed by NM, 30-Apr-2015.)
⊢ Fun ◡{⟨𝐴, 𝐵⟩}
Theorem	funsng 6551	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 28-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {⟨𝐴, 𝐵⟩})
Theorem	fnsng 6552	Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩} Fn {𝐴})
Theorem	funsn 6553	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 12-Aug-1994.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ Fun {⟨𝐴, 𝐵⟩}
Theorem	funprg 6554	A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → Fun {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩})
Theorem	funtpg 6555	A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩})
Theorem	funpr 6556	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → Fun {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩})
Theorem	funtp 6557	A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
Theorem	fnsn 6558	Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {⟨𝐴, 𝐵⟩} Fn {𝐴}
Theorem	fnprg 6559	Function with a domain of two different values. (Contributed by FL, 26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} Fn {𝐴, 𝐵})
Theorem	fntpg 6560	Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩} Fn {𝑋, 𝑌, 𝑍})
Theorem	fntp 6561	A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} Fn {𝐴, 𝐵, 𝐶})
Theorem	funcnvpr 6562	The converse pair of ordered pairs is a function if the second members are different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩})
Theorem	funcnvtp 6563	The converse triple of ordered pairs is a function if the second members are pairwise different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩})
Theorem	funcnvqp 6564	The converse quadruple of ordered pairs is a function if the second members are pairwise different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ {⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}))
Theorem	fun0 6565	The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by NM, 7-Apr-1998.)
⊢ Fun ∅
Theorem	funcnv0 6566	The converse of the empty set is a function. (Contributed by AV, 7-Jan-2021.)
⊢ Fun ◡∅
Theorem	funcnvcnv 6567	The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.)
⊢ (Fun 𝐴 → Fun ◡◡𝐴)
Theorem	funcnv2 6568*	A simpler equivalence for single-rooted (see funcnv 6569). (Contributed by NM, 9-Aug-2004.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦∃*𝑥 𝑥𝐴𝑦)
Theorem	funcnv 6569*	The converse of a class is a function iff the class is single-rooted, which means that for any 𝑦 in the range of 𝐴 there is at most one 𝑥 such that 𝑥𝐴𝑦. Definition of single-rooted in [Enderton] p. 43. See funcnv2 6568 for a simpler version. (Contributed by NM, 13-Aug-2004.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃*𝑥 𝑥𝐴𝑦)
Theorem	funcnv3 6570*	A condition showing a class is single-rooted. (See funcnv 6569). (Contributed by NM, 26-May-2006.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃!𝑥 ∈ dom 𝐴 𝑥𝐴𝑦)
Theorem	fun2cnv 6571*	The double converse of a class is a function iff the class is single-valued. Each side is equivalent to Definition 6.4(2) of [TakeutiZaring] p. 23, who use the notation "Un(A)" for single-valued. Note that 𝐴 is not necessarily a function. (Contributed by NM, 13-Aug-2004.)
⊢ (Fun ◡◡𝐴 ↔ ∀𝑥∃*𝑦 𝑥𝐴𝑦)
Theorem	svrelfun 6572	A single-valued relation is a function. (See fun2cnv 6571 for "single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 17-Jan-2006.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ Fun ◡◡𝐴))
Theorem	fncnv 6573*	Single-rootedness (see funcnv 6569) of a class cut down by a Cartesian product. (Contributed by NM, 5-Mar-2007.)
⊢ (◡(𝑅 ∩ (𝐴 × 𝐵)) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑥𝑅𝑦)
Theorem	fun11 6574*	Two ways of stating that 𝐴 is one-to-one (but not necessarily a function). Each side is equivalent to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation "Un2 (A)" for one-to-one (but not necessarily a function). (Contributed by NM, 17-Jan-2006.)
⊢ ((Fun ◡◡𝐴 ∧ Fun ◡𝐴) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑤) → (𝑥 = 𝑧 ↔ 𝑦 = 𝑤)))
Theorem	fununi 6575*	The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ 𝐴)
Theorem	funin 6576	The intersection with a function is a function. Exercise 14(a) of [Enderton] p. 53. (Contributed by NM, 19-Mar-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (Fun 𝐹 → Fun (𝐹 ∩ 𝐺))
Theorem	funres11 6577	The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998.)
⊢ (Fun ◡𝐹 → Fun ◡(𝐹 ↾ 𝐴))
Theorem	funcnvres 6578	The converse of a restricted function. (Contributed by NM, 27-Mar-1998.)
⊢ (Fun ◡𝐹 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ (𝐹 “ 𝐴)))
Theorem	cnvresid 6579	Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.)
⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
Theorem	funcnvres2 6580	The converse of a restriction of the converse of a function equals the function restricted to the image of its converse. (Contributed by NM, 4-May-2005.)
⊢ (Fun 𝐹 → ◡(◡𝐹 ↾ 𝐴) = (𝐹 ↾ (◡𝐹 “ 𝐴)))
Theorem	funimacnv 6581	The image of the preimage of a function. (Contributed by NM, 25-May-2004.)
⊢ (Fun 𝐹 → (𝐹 “ (◡𝐹 “ 𝐴)) = (𝐴 ∩ ran 𝐹))
Theorem	funimass1 6582	A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by NM, 25-May-2004.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹) → ((◡𝐹 “ 𝐴) ⊆ 𝐵 → 𝐴 ⊆ (𝐹 “ 𝐵)))
Theorem	funimass2 6583	A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by NM, 25-May-2004.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ (◡𝐹 “ 𝐵)) → (𝐹 “ 𝐴) ⊆ 𝐵)
Theorem	imadif 6584	The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
Theorem	imain 6585	The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))
Theorem	f1imadifssran 6586	Condition for the range of a one-to-one function to be the range of one its restrictions. Variant of imadifssran 6117. (Contributed by AV, 4-Oct-2025.)
⊢ (Fun ◡𝐹 → ((𝐹 “ (dom 𝐹 ∖ 𝐴)) ⊆ ran (𝐹 ↾ 𝐴) → ran 𝐹 = ran (𝐹 ↾ 𝐴)))
Theorem	funimaexg 6587	Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 10-Sep-2006.) Shorten proof and avoid ax-10 2147, ax-12 2185. (Revised by SN, 19-Dec-2024.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 “ 𝐵) ∈ V)
Theorem	funimaex 6588	The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep 5226. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 17-Nov-2002.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (Fun 𝐴 → (𝐴 “ 𝐵) ∈ V)
Theorem	isarep1 6589*	Part of a study of the Axiom of Replacement used by the Isabelle prover. The object PrimReplace is apparently the image of the function encoded by 𝜑(𝑥, 𝑦) i.e. the class ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴). If so, we can prove Isabelle's "Axiom of Replacement" conclusion without using the Axiom of Replacement, for which I (N. Megill) currently have no explanation. (Contributed by NM, 26-Oct-2006.) (Proof shortened by Mario Carneiro, 4-Dec-2016.) (Proof shortened by SN, 19-Dec-2024.)
⊢ (𝑏 ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 [𝑏 / 𝑦]𝜑)
Theorem	isarep2 6590*	Part of a study of the Axiom of Replacement used by the Isabelle prover. In Isabelle, the sethood of PrimReplace is apparently postulated implicitly by its type signature "[ i, [ i, i ] => o ] => i", which automatically asserts that it is a set without using any axioms. To prove that it is a set in Metamath, we need the hypotheses of Isabelle's "Axiom of Replacement" as well as the Axiom of Replacement in the form funimaex 6588. (Contributed by NM, 26-Oct-2006.)
⊢ 𝐴 ∈ V    &   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧((𝜑 ∧ [𝑧 / 𝑦]𝜑) → 𝑦 = 𝑧)    ⇒   ⊢ ∃𝑤 𝑤 = ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴)
Theorem	fneq1 6591	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
Theorem	fneq2 6592	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
Theorem	fneq1d 6593	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
Theorem	fneq2d 6594	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
Theorem	fneq12d 6595	Equality deduction for function predicate with domain. (Contributed by NM, 26-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵))
Theorem	fneq12 6596	Equality theorem for function predicate with domain. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵))
Theorem	fneq1i 6597	Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)
Theorem	fneq2i 6598	Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)
Theorem	nffn 6599	Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐹 Fn 𝐴
Theorem	fnfun 6600	A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → Fun 𝐹)