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	fntpg 6501	Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩} Fn {𝑋, 𝑌, 𝑍})
Theorem	fntp 6502	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 6503	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 6504	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 6505	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 6506	The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by NM, 7-Apr-1998.)
⊢ Fun ∅
Theorem	funcnv0 6507	The converse of the empty set is a function. (Contributed by AV, 7-Jan-2021.)
⊢ Fun ◡∅
Theorem	funcnvcnv 6508	The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.)
⊢ (Fun 𝐴 → Fun ◡◡𝐴)
Theorem	funcnv2 6509*	A simpler equivalence for single-rooted (see funcnv 6510). (Contributed by NM, 9-Aug-2004.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦∃*𝑥 𝑥𝐴𝑦)
Theorem	funcnv 6510*	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 6509 for a simpler version. (Contributed by NM, 13-Aug-2004.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃*𝑥 𝑥𝐴𝑦)
Theorem	funcnv3 6511*	A condition showing a class is single-rooted. (See funcnv 6510). (Contributed by NM, 26-May-2006.)
⊢ (Fun ◡𝐴 ↔ ∀𝑦 ∈ ran 𝐴∃!𝑥 ∈ dom 𝐴 𝑥𝐴𝑦)
Theorem	fun2cnv 6512*	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 6513	A single-valued relation is a function. (See fun2cnv 6512 for "single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 17-Jan-2006.)
⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ Fun ◡◡𝐴))
Theorem	fncnv 6514*	Single-rootedness (see funcnv 6510) of a class cut down by a Cartesian product. (Contributed by NM, 5-Mar-2007.)
⊢ (◡(𝑅 ∩ (𝐴 × 𝐵)) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑥𝑅𝑦)
Theorem	fun11 6515*	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 6516*	The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪ 𝐴)
Theorem	funin 6517	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 6518	The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998.)
⊢ (Fun ◡𝐹 → Fun ◡(𝐹 ↾ 𝐴))
Theorem	funcnvres 6519	The converse of a restricted function. (Contributed by NM, 27-Mar-1998.)
⊢ (Fun ◡𝐹 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ (𝐹 “ 𝐴)))
Theorem	cnvresid 6520	Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.)
⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
Theorem	funcnvres2 6521	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 6522	The image of the preimage of a function. (Contributed by NM, 25-May-2004.)
⊢ (Fun 𝐹 → (𝐹 “ (◡𝐹 “ 𝐴)) = (𝐴 ∩ ran 𝐹))
Theorem	funimass1 6523	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 6524	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 6525	The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
Theorem	imain 6526	The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))
Theorem	funimaexg 6527	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 2138, ax-12 2172. (Revised by SN, 19-Dec-2024.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 “ 𝐵) ∈ V)
Theorem	funimaexgOLD 6528	Obsolete version of funimaexg 6527 as of 19-Dec-2024. (Contributed by NM, 10-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 “ 𝐵) ∈ V)
Theorem	funimaex 6529	The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep 5210. 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 6530*	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	isarep1OLD 6531*	Obsolete version of isarep1 6530 as of 19-Dec-2024. (Contributed by NM, 26-Oct-2006.) (Proof shortened by Mario Carneiro, 4-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑏 ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 [𝑏 / 𝑦]𝜑)
Theorem	isarep2 6532*	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 6529. (Contributed by NM, 26-Oct-2006.)
⊢ 𝐴 ∈ V    &   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧((𝜑 ∧ [𝑧 / 𝑦]𝜑) → 𝑦 = 𝑧)    ⇒   ⊢ ∃𝑤 𝑤 = ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴)
Theorem	fneq1 6533	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
Theorem	fneq2 6534	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
Theorem	fneq1d 6535	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
Theorem	fneq2d 6536	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
Theorem	fneq12d 6537	Equality deduction for function predicate with domain. (Contributed by NM, 26-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵))
Theorem	fneq12 6538	Equality theorem for function predicate with domain. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐵))
Theorem	fneq1i 6539	Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)
Theorem	fneq2i 6540	Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)
Theorem	nffn 6541	Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐹 Fn 𝐴
Theorem	fnfun 6542	A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
Theorem	fnfund 6543	A function with domain is a function, deduction form. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	fnrel 6544	A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
Theorem	fndm 6545	The domain of a function. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Theorem	fndmi 6546	The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.)
⊢ 𝐹 Fn 𝐴    ⇒   ⊢ dom 𝐹 = 𝐴
Theorem	fndmd 6547	The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → dom 𝐹 = 𝐴)
Theorem	funfni 6548	Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)
Theorem	fndmu 6549	A function has a unique domain. (Contributed by NM, 11-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐵) → 𝐴 = 𝐵)
Theorem	fnbr 6550	The first argument of binary relation on a function belongs to the function's domain. (Contributed by NM, 7-May-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵𝐹𝐶) → 𝐵 ∈ 𝐴)
Theorem	fnop 6551	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 6552*	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 6553*	There is exactly one value of a function. (Contributed by NM, 7-Nov-1995.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑦⟨𝐵, 𝑦⟩ ∈ 𝐹)
Theorem	fnun 6554	The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))
Theorem	fnund 6555	The union of two functions with disjoint domains, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))
Theorem	fnunop 6556	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 6557	Composition of a function with domain and a function as a function with domain. Generalization of fnco 6558. (Contributed by AV, 17-Sep-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺) Fn (◡𝐺 “ 𝐴))
Theorem	fnco 6558	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	fncoOLD 6559	Obsolete version of fnco 6558 as of 20-Sep-2024. (Contributed by NM, 22-May-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵)
Theorem	fnresdm 6560	A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
Theorem	fnresdisj 6561	A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004.)
⊢ (𝐹 Fn 𝐴 → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐹 ↾ 𝐵) = ∅))
Theorem	2elresin 6562	Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐺 ↾ (𝐴 ∩ 𝐵)))))
Theorem	fnssresb 6563	Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007.)
⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴))
Theorem	fnssres 6564	Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)
Theorem	fnssresd 6565	Restriction of a function to a subclass of its domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐵) Fn 𝐵)
Theorem	fnresin1 6566	Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐴 ∩ 𝐵)) Fn (𝐴 ∩ 𝐵))
Theorem	fnresin2 6567	Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐵 ∩ 𝐴)) Fn (𝐵 ∩ 𝐴))
Theorem	fnres 6568*	An equivalence for functionality of a restriction. Compare dffun8 6469. (Contributed by Mario Carneiro, 20-May-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)
Theorem	idfn 6569	The identity relation is a function on the universal class. See also funi 6473. (Contributed by BJ, 23-Dec-2023.)
⊢ I Fn V
Theorem	fnresi 6570	The restricted identity relation is a function on the restricting class. (Contributed by NM, 27-Aug-2004.) (Proof shortened by BJ, 27-Dec-2023.)
⊢ ( I ↾ 𝐴) Fn 𝐴
Theorem	fnresiOLD 6571	Obsolete proof of fnresi 6570 as of 27-Dec-2023. (Contributed by NM, 27-Aug-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ( I ↾ 𝐴) Fn 𝐴
Theorem	fnima 6572	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 𝐹)
Theorem	fn0 6573	A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)
Theorem	fnimadisj 6574	A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐹 Fn 𝐴 ∧ (𝐴 ∩ 𝐶) = ∅) → (𝐹 “ 𝐶) = ∅)
Theorem	fnimaeq0 6575	Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 40883. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 “ 𝐵) = ∅ ↔ 𝐵 = ∅))
Theorem	dfmpt3 6576	Alternate definition for the maps-to notation df-mpt 5159. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝐵})
Theorem	mptfnf 6577	The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
Theorem	fnmptf 6578	The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) (Revised by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
Theorem	fnopabg 6579*	Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ↔ 𝐹 Fn 𝐴)
Theorem	fnopab 6580*	Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 5-Mar-1996.)
⊢ (𝑥 ∈ 𝐴 → ∃!𝑦𝜑)    &   ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}    ⇒   ⊢ 𝐹 Fn 𝐴
Theorem	mptfng 6581*	The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
Theorem	fnmpt 6582*	The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)
Theorem	fnmptd 6583*	The maps-to notation defines a function with domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 Fn 𝐴)
Theorem	mpt0 6584	A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅
Theorem	fnmpti 6585*	Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ 𝐹 Fn 𝐴
Theorem	dmmpti 6586*	Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 = 𝐴
Theorem	dmmptd 6587*	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐴 = 𝐵)
Theorem	mptun 6588	Union of mappings which are mutually compatible. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ∪ (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	partfun 6589	Rewrite a function defined by parts, using a mapping and an if construct, into a union of functions on disjoint domains. (Contributed by Thierry Arnoux, 30-Mar-2017.)
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) = ((𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶) ∪ (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ 𝐷))
Theorem	feq1 6590	Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
Theorem	feq2 6591	Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
Theorem	feq3 6592	Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵))
Theorem	feq23 6593	Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))
Theorem	feq1d 6594	Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
Theorem	feq2d 6595	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
Theorem	feq3d 6596	Equality deduction for functions. (Contributed by AV, 1-Jan-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))
Theorem	feq12d 6597	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶))
Theorem	feq123d 6598	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐷))
Theorem	feq123 6599	Equality theorem for functions. (Contributed by FL, 16-Nov-2008.)
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐶⟶𝐷))
Theorem	feq1i 6600	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)