P. 55 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5401-5500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	funeu2 5401*	There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.)
⊢ ((Fun 𝐹 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐹) → ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹)
Theorem	dffun7 5402*	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 5403 shows that it does not matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
Theorem	dffun8 5403*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 5402. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃!𝑦 𝑥𝐴𝑦))
Theorem	dffun9 5404*	Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 ∈ ran 𝐴 𝑥𝐴𝑦))
Theorem	funfn 5405	An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)
Theorem	funfnd 5406	A function is a function over its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → Fun 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 Fn dom 𝐴)
Theorem	funi 5407	The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. (Contributed by NM, 30-Apr-1998.)
⊢ Fun I
Theorem	nfunv 5408	The universe is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
⊢ ¬ Fun V
Theorem	funopg 5409	A Kuratowski ordered pair is a function only if its components are equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun ⟨𝐴, 𝐵⟩) → 𝐴 = 𝐵)
Theorem	funopab 5410*	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 5411*	A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐴}
Theorem	funopab4 5412*	A class of ordered pairs of values in the form used by df-mpt 4192 is a function. (Contributed by NM, 17-Feb-2013.)
⊢ Fun {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝑦 = 𝐴)}
Theorem	funmpt 5413	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	funmpt2 5414	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 5415	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	funres 5416	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 5417	A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ (𝜑 → Fun (𝐹 ↾ 𝐴))
Theorem	funssres 5418	The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺)
Theorem	fun2ssres 5419	Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ⊆ dom 𝐺) → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴))
Theorem	funun 5420	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 5421*	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 5422	If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019.)
⊢ (Fun (𝐹 ∪ 𝐺) → (Fun 𝐹 ∧ Fun 𝐺))
Theorem	fundif 5423	A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021.)
⊢ (Fun 𝐹 → Fun (𝐹 ∖ 𝐴))
Theorem	funcnvsn 5424	The converse singleton of an ordered pair is a function. This is equivalent to funsn 5427 via cnvsn 5268, but stating it this way allows us to skip the sethood assumptions on 𝐴 and 𝐵. (Contributed by NM, 30-Apr-2015.)
⊢ Fun ◡{⟨𝐴, 𝐵⟩}
Theorem	funsng 5425	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 5426	Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩} Fn {𝐴})
Theorem	funsn 5427	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	funinsn 5428	A function based on the singleton of an ordered pair. Unlike funsng 5425, this holds even if 𝐴 or 𝐵 is a proper class. (Contributed by Jim Kingdon, 17-Apr-2022.)
⊢ Fun ({⟨𝐴, 𝐵⟩} ∩ (𝑉 × 𝑊))
Theorem	funprg 5429	A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → Fun {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩})
Theorem	funtpg 5430	A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩})
Theorem	funpr 5431	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → Fun {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩})
Theorem	funtp 5432	A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
Theorem	fnsn 5433	Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {⟨𝐴, 𝐵⟩} Fn {𝐴}
Theorem	fnprg 5434	Function with a domain of two different values. (Contributed by FL, 26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} Fn {𝐴, 𝐵})
Theorem	fntpg 5435	Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩} Fn {𝑋, 𝑌, 𝑍})
Theorem	fntp 5436	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	fun0 5437	The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by NM, 7-Apr-1998.)
⊢ Fun ∅
Theorem	funcnvcnv 5438	The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.)
⊢ (Fun 𝐴 → Fun ◡◡𝐴)
Theorem	funcnv2 5439*	A simpler equivalence for single-rooted (see funcnv 5440). (Contributed by NM, 9-Aug-2004.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦∃*𝑥 𝑥𝐴𝑦)
Theorem	funcnv 5440*	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 5439 for a simpler version. (Contributed by NM, 13-Aug-2004.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃*𝑥 𝑥𝐴𝑦)
Theorem	funcnv3 5441*	A condition showing a class is single-rooted. (See funcnv 5440). (Contributed by NM, 26-May-2006.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃!𝑥 ∈ dom 𝐴 𝑥𝐴𝑦)
Theorem	funcnveq 5442*	Another way of expressing that a class is single-rooted. Counterpart to dffun2 5385. (Contributed by Jim Kingdon, 24-Dec-2018.)
⊢ (Fun ◡𝐴 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑧𝐴𝑦) → 𝑥 = 𝑧))
Theorem	fun2cnv 5443*	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 5444	A single-valued relation is a function. (See fun2cnv 5443 for "single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 17-Jan-2006.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ Fun ◡◡𝐴))
Theorem	fncnv 5445*	Single-rootedness (see funcnv 5440) of a class cut down by a cross product. (Contributed by NM, 5-Mar-2007.)
⊢ (◡(𝑅 ∩ (𝐴 × 𝐵)) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑥𝑅𝑦)
Theorem	fun11 5446*	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 5447*	The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ 𝐴)
Theorem	funcnvuni 5448*	The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 5440 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴)
Theorem	fun11uni 5449*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by NM, 11-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 ((Fun 𝑓 ∧ Fun ◡𝑓) ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ∪ 𝐴 ∧ Fun ◡∪ 𝐴))
Theorem	funin 5450	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 5451	The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998.)
⊢ (Fun ◡𝐹 → Fun ◡(𝐹 ↾ 𝐴))
Theorem	funcnvres 5452	The converse of a restricted function. (Contributed by NM, 27-Mar-1998.)
⊢ (Fun ◡𝐹 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ (𝐹 “ 𝐴)))
Theorem	cnvresid 5453	Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.)
⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
Theorem	funcnvres2 5454	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 5455	The image of the preimage of a function. (Contributed by NM, 25-May-2004.)
⊢ (Fun 𝐹 → (𝐹 “ (◡𝐹 “ 𝐴)) = (𝐴 ∩ ran 𝐹))
Theorem	funimass1 5456	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 5457	A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by NM, 25-May-2004.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ (◡𝐹 “ 𝐵)) → (𝐹 “ 𝐴) ⊆ 𝐵)
Theorem	imadiflem 5458	One direction of imadif 5459. This direction does not require Fun ◡𝐹. (Contributed by Jim Kingdon, 25-Dec-2018.)
⊢ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ⊆ (𝐹 “ (𝐴 ∖ 𝐵))
Theorem	imadif 5459	The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
Theorem	imainlem 5460	One direction of imain 5461. This direction does not require Fun ◡𝐹. (Contributed by Jim Kingdon, 25-Dec-2018.)
⊢ (𝐹 “ (𝐴 ∩ 𝐵)) ⊆ ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵))
Theorem	imain 5461	The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))
Theorem	funimaexglem 5462	Lemma for funimaexg 5463. It constitutes the interesting part of funimaexg 5463, in which 𝐵 ⊆ dom 𝐴. (Contributed by Jim Kingdon, 27-Dec-2018.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ dom 𝐴) → (𝐴 “ 𝐵) ∈ V)
Theorem	funimaexg 5463	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.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 “ 𝐵) ∈ V)
Theorem	funimaex 5464	The image of a set under any function is also a set. Equivalent of Axiom of Replacement. 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 5465*	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.)
⊢ (𝑏 ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 [𝑏 / 𝑦]𝜑)
Theorem	isarep2 5466*	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 5464. (Contributed by NM, 26-Oct-2006.)
⊢ 𝐴 ∈ V    &   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧((𝜑 ∧ [𝑧 / 𝑦]𝜑) → 𝑦 = 𝑧)    ⇒   ⊢ ∃𝑤 𝑤 = ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴)
Theorem	fneq1 5467	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
Theorem	fneq2 5468	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
Theorem	fneq1d 5469	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
Theorem	fneq2d 5470	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
Theorem	fneq12d 5471	Equality deduction for function predicate with domain. (Contributed by NM, 26-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵))
Theorem	fneq12 5472	Equality theorem for function predicate with domain. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵))
Theorem	fneq1i 5473	Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)
Theorem	fneq2i 5474	Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)
Theorem	nffn 5475	Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐹 Fn 𝐴
Theorem	fnfun 5476	A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
Theorem	fnrel 5477	A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
Theorem	fndm 5478	The domain of a function. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Theorem	fndmi 5479	The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.)
⊢ 𝐹 Fn 𝐴    ⇒   ⊢ dom 𝐹 = 𝐴
Theorem	fndmd 5480	The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → dom 𝐹 = 𝐴)
Theorem	funfni 5481	Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)
Theorem	fndmu 5482	A function has a unique domain. (Contributed by NM, 11-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐵) → 𝐴 = 𝐵)
Theorem	fnbr 5483	The first argument of binary relation on a function belongs to the function's domain. (Contributed by NM, 7-May-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵𝐹𝐶) → 𝐵 ∈ 𝐴)
Theorem	fnop 5484	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 5485*	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 5486*	There is exactly one value of a function. (Contributed by NM, 7-Nov-1995.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑦⟨𝐵, 𝑦⟩ ∈ 𝐹)
Theorem	fnun 5487	The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))
Theorem	fnunsn 5488	Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝜑 → 𝑋 ∈ V)    &   ⊢ (𝜑 → 𝑌 ∈ V)    &   ⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ 𝐺 = (𝐹 ∪ {⟨𝑋, 𝑌⟩})    &   ⊢ 𝐸 = (𝐷 ∪ {𝑋})    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝐺 Fn 𝐸)
Theorem	fnco 5489	Composition of two functions. (Contributed by NM, 22-May-2006.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵)
Theorem	fnresdm 5490	A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
Theorem	fnresdisj 5491	A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004.)
⊢ (𝐹 Fn 𝐴 → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐹 ↾ 𝐵) = ∅))
Theorem	2elresin 5492	Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐺 ↾ (𝐴 ∩ 𝐵)))))
Theorem	fnssresb 5493	Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007.)
⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴))
Theorem	fnssres 5494	Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)
Theorem	fnssresd 5495	Restriction of a function to a subclass of its domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐵) Fn 𝐵)
Theorem	fnresin1 5496	Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐴 ∩ 𝐵)) Fn (𝐴 ∩ 𝐵))
Theorem	fnresin2 5497	Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐵 ∩ 𝐴)) Fn (𝐵 ∩ 𝐴))
Theorem	fnres 5498*	An equivalence for functionality of a restriction. Compare dffun8 5403. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)
Theorem	fnresi 5499	Functionality and domain of restricted identity. (Contributed by NM, 27-Aug-2004.)
⊢ ( I ↾ 𝐴) Fn 𝐴
Theorem	fnima 5500	The image of a function's domain is its range. (Contributed by NM, 4-Nov-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹)