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	sbcfung 6501	Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Fun 𝐹 ↔ Fun ⦋𝐴 / 𝑥⦌𝐹))
Theorem	funeu 6502*	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 6503*	There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.)
⊢ ((Fun 𝐹 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐹) → ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹)
Theorem	dffun7 6504*	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 6505 shows that it does not matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
Theorem	dffun8 6505*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 6504. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦))
Theorem	dffun9 6506*	Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 ∈ ran 𝐴 𝑥𝐴𝑦))
Theorem	funfn 6507	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 6508	A function is a function on its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → Fun 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 Fn dom 𝐴)
Theorem	funi 6509	The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. See also idfn 6605. (Contributed by NM, 30-Apr-1998.)
⊢ Fun I
Theorem	nfunv 6510	The universal class is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
⊢ ¬ Fun V
Theorem	funopg 6511	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 6528, as relsnopg 5741 is to relop 5788. (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun ⟨𝐴, 𝐵⟩) → 𝐴 = 𝐵)
Theorem	funopab 6512*	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 6513*	A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐴}
Theorem	funopab4 6514*	A class of ordered pairs of values in the form used by df-mpt 5171 is a function. (Contributed by NM, 17-Feb-2013.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝑦 = 𝐴)}
Theorem	funmpt 6515	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	funmpt2 6516	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 6517	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 6518	Composition of two functions, generalization of funco 6517. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
⊢ ((Fun (𝐹 ↾ ran 𝐺) ∧ Fun 𝐺) → Fun (𝐹 ∘ 𝐺))
Theorem	funres 6519	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 6520	A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → Fun (𝐹 ↾ 𝐴))
Theorem	funssres 6521	The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺)
Theorem	fun2ssres 6522	Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ⊆ dom 𝐺) → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴))
Theorem	funun 6523	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 6524*	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 6525	If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019.)
⊢ (Fun (𝐹 ∪ 𝐺) → (Fun 𝐹 ∧ Fun 𝐺))
Theorem	fundif 6526	A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021.)
⊢ (Fun 𝐹 → Fun (𝐹 ∖ 𝐴))
Theorem	funcnvsn 6527	The converse singleton of an ordered pair is a function. This is equivalent to funsn 6530 via cnvsn 6170, but stating it this way allows to skip the sethood assumptions on 𝐴 and 𝐵. (Contributed by NM, 30-Apr-2015.)
⊢ Fun ◡{⟨𝐴, 𝐵⟩}
Theorem	funsng 6528	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 6529	Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩} Fn {𝐴})
Theorem	funsn 6530	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 6531	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 6532	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 6533	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → Fun {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩})
Theorem	funtp 6534	A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
Theorem	fnsn 6535	Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {⟨𝐴, 𝐵⟩} Fn {𝐴}
Theorem	fnprg 6536	Function with a domain of two different values. (Contributed by FL, 26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} Fn {𝐴, 𝐵})
Theorem	fntpg 6537	Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩} Fn {𝑋, 𝑌, 𝑍})
Theorem	fntp 6538	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 6539	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 6540	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 6541	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 6542	The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by NM, 7-Apr-1998.)
⊢ Fun ∅
Theorem	funcnv0 6543	The converse of the empty set is a function. (Contributed by AV, 7-Jan-2021.)
⊢ Fun ◡∅
Theorem	funcnvcnv 6544	The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.)
⊢ (Fun 𝐴 → Fun ◡◡𝐴)
Theorem	funcnv2 6545*	A simpler equivalence for single-rooted (see funcnv 6546). (Contributed by NM, 9-Aug-2004.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦∃*𝑥 𝑥𝐴𝑦)
Theorem	funcnv 6546*	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 6545 for a simpler version. (Contributed by NM, 13-Aug-2004.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃*𝑥 𝑥𝐴𝑦)
Theorem	funcnv3 6547*	A condition showing a class is single-rooted. (See funcnv 6546). (Contributed by NM, 26-May-2006.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃!𝑥 ∈ dom 𝐴 𝑥𝐴𝑦)
Theorem	fun2cnv 6548*	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 6549	A single-valued relation is a function. (See fun2cnv 6548 for "single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 17-Jan-2006.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ Fun ◡◡𝐴))
Theorem	fncnv 6550*	Single-rootedness (see funcnv 6546) of a class cut down by a Cartesian product. (Contributed by NM, 5-Mar-2007.)
⊢ (◡(𝑅 ∩ (𝐴 × 𝐵)) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑥𝑅𝑦)
Theorem	fun11 6551*	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 6552*	The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ 𝐴)
Theorem	funin 6553	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 6554	The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998.)
⊢ (Fun ◡𝐹 → Fun ◡(𝐹 ↾ 𝐴))
Theorem	funcnvres 6555	The converse of a restricted function. (Contributed by NM, 27-Mar-1998.)
⊢ (Fun ◡𝐹 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ (𝐹 “ 𝐴)))
Theorem	cnvresid 6556	Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.)
⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
Theorem	funcnvres2 6557	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 6558	The image of the preimage of a function. (Contributed by NM, 25-May-2004.)
⊢ (Fun 𝐹 → (𝐹 “ (◡𝐹 “ 𝐴)) = (𝐴 ∩ ran 𝐹))
Theorem	funimass1 6559	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 6560	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 6561	The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
Theorem	imain 6562	The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))
Theorem	f1imadifssran 6563	Condition for the range of a one-to-one function to be the range of one its restrictions. Variant of imadifssran 6095. (Contributed by AV, 4-Oct-2025.)
⊢ (Fun ◡𝐹 → ((𝐹 “ (dom 𝐹 ∖ 𝐴)) ⊆ ran (𝐹 ↾ 𝐴) → ran 𝐹 = ran (𝐹 ↾ 𝐴)))
Theorem	funimaexg 6564	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 2143, ax-12 2179. (Revised by SN, 19-Dec-2024.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 “ 𝐵) ∈ V)
Theorem	funimaex 6565	The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep 5215. 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 6566*	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 6567*	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 6565. (Contributed by NM, 26-Oct-2006.)
⊢ 𝐴 ∈ V    &   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧((𝜑 ∧ [𝑧 / 𝑦]𝜑) → 𝑦 = 𝑧)    ⇒   ⊢ ∃𝑤 𝑤 = ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴)
Theorem	fneq1 6568	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
Theorem	fneq2 6569	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
Theorem	fneq1d 6570	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
Theorem	fneq2d 6571	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
Theorem	fneq12d 6572	Equality deduction for function predicate with domain. (Contributed by NM, 26-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵))
Theorem	fneq12 6573	Equality theorem for function predicate with domain. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵))
Theorem	fneq1i 6574	Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)
Theorem	fneq2i 6575	Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)
Theorem	nffn 6576	Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐹 Fn 𝐴
Theorem	fnfun 6577	A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
Theorem	fnfund 6578	A function with domain is a function, deduction form. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	fnrel 6579	A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
Theorem	fndm 6580	The domain of a function. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Theorem	fndmi 6581	The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.)
⊢ 𝐹 Fn 𝐴    ⇒   ⊢ dom 𝐹 = 𝐴
Theorem	fndmd 6582	The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → dom 𝐹 = 𝐴)
Theorem	funfni 6583	Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)
Theorem	fndmu 6584	A function has a unique domain. (Contributed by NM, 11-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐵) → 𝐴 = 𝐵)
Theorem	fnbr 6585	The first argument of binary relation on a function belongs to the function's domain. (Contributed by NM, 7-May-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵𝐹𝐶) → 𝐵 ∈ 𝐴)
Theorem	fnop 6586	The first argument of an ordered pair in a function belongs to the function's domain. (Contributed by NM, 8-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝐹) → 𝐵 ∈ 𝐴)
Theorem	fneu 6587*	There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑦 𝐵𝐹𝑦)
Theorem	fneu2 6588*	There is exactly one value of a function. (Contributed by NM, 7-Nov-1995.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑦⟨𝐵, 𝑦⟩ ∈ 𝐹)
Theorem	fnunres1 6589	Restriction of a disjoint union to the domain of the first function. (Contributed by Thierry Arnoux, 9-Dec-2021.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 ∪ 𝐺) ↾ 𝐴) = 𝐹)
Theorem	fnunres2 6590	Restriction of a disjoint union to the domain of the second function. (Contributed by Thierry Arnoux, 12-Oct-2023.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺)
Theorem	fnun 6591	The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))
Theorem	fnund 6592	The union of two functions with disjoint domains, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))
Theorem	fnunop 6593	Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by AV, 16-Aug-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ 𝐺 = (𝐹 ∪ {⟨𝑋, 𝑌⟩})    &   ⊢ 𝐸 = (𝐷 ∪ {𝑋})    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝐺 Fn 𝐸)
Theorem	fncofn 6594	Composition of a function with domain and a function as a function with domain. Generalization of fnco 6595. (Contributed by AV, 17-Sep-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
Theorem	fnco 6595	Composition of two functions with domains as a function with domain. (Contributed by NM, 22-May-2006.) (Proof shortened by AV, 20-Sep-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵)
Theorem	fnresdm 6596	A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
Theorem	fnresdisj 6597	A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004.)
⊢ (𝐹 Fn 𝐴 → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐹 ↾ 𝐵) = ∅))
Theorem	2elresin 6598	Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐺 ↾ (𝐴 ∩ 𝐵)))))
Theorem	fnssresb 6599	Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007.)
⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴))
Theorem	fnssres 6600	Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)