P. 60 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5901-6000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nffn 5901	Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝐹 Fn 𝐴
Theorem	fnfun 5902	A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
Theorem	fnrel 5903	A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
Theorem	fndm 5904	The domain of a function. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Theorem	funfni 5905	Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑)    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑)
Theorem	fndmu 5906	A function has a unique domain. (Contributed by NM, 11-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐵) → 𝐴 = 𝐵)
Theorem	fnbr 5907	The first argument of binary relation on a function belongs to the function's domain. (Contributed by NM, 7-May-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵𝐹𝐶) → 𝐵 ∈ 𝐴)
Theorem	fnop 5908	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 5909*	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 5910*	There is exactly one value of a function. (Contributed by NM, 7-Nov-1995.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑦⟨𝐵, 𝑦⟩ ∈ 𝐹)
Theorem	fnun 5911	The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))
Theorem	fnunsn 5912	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 5913	Composition of two functions. (Contributed by NM, 22-May-2006.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵)
Theorem	fnresdm 5914	A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
Theorem	fnresdisj 5915	A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004.)
⊢ (𝐹 Fn 𝐴 → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐹 ↾ 𝐵) = ∅))
Theorem	2elresin 5916	Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐺 ↾ (𝐴 ∩ 𝐵)))))
Theorem	fnssresb 5917	Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007.)
⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴))
Theorem	fnssres 5918	Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵)
Theorem	fnresin1 5919	Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐴 ∩ 𝐵)) Fn (𝐴 ∩ 𝐵))
Theorem	fnresin2 5920	Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐵 ∩ 𝐴)) Fn (𝐵 ∩ 𝐴))
Theorem	fnres 5921*	An equivalence for functionality of a restriction. Compare dffun8 5831. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)
Theorem	fnresi 5922	Functionality and domain of restricted identity. (Contributed by NM, 27-Aug-2004.)
⊢ ( I ↾ 𝐴) Fn 𝐴
Theorem	fnima 5923	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 5924	A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅)
Theorem	fnimadisj 5925	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 5926	Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 36639. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 “ 𝐵) = ∅ ↔ 𝐵 = ∅))
Theorem	dfmpt3 5927	Alternate definition for the "maps to" notation df-mpt 4645. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝐵})
Theorem	mptfnf 5928	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 5929	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 5930*	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 5931*	Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 5-Mar-1996.)
⊢ (𝑥 ∈ 𝐴 → ∃!𝑦𝜑)    &   ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}    ⇒   ⊢ 𝐹 Fn 𝐴
Theorem	mptfng 5932*	The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
Theorem	fnmpt 5933*	The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)
Theorem	mpt0 5934	A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅
Theorem	fnmpti 5935*	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 5936*	Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 = 𝐴
Theorem	dmmptd 5937*	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐴 = 𝐵)
Theorem	mptun 5938	Union of mappings which are mutually compatible. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ∪ (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	feq1 5939	Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
Theorem	feq2 5940	Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
Theorem	feq3 5941	Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵))
Theorem	feq23 5942	Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))
Theorem	feq1d 5943	Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
Theorem	feq2d 5944	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
Theorem	feq3d 5945	Equality deduction for functions. (Contributed by AV, 1-Jan-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))
Theorem	feq12d 5946	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶))
Theorem	feq123d 5947	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐷))
Theorem	feq123 5948	Equality theorem for functions. (Contributed by FL, 16-Nov-2008.)
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐶⟶𝐷))
Theorem	feq1i 5949	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)
Theorem	feq2i 5950	Equality inference for functions. (Contributed by NM, 5-Sep-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)
Theorem	feq12i 5951	Equality inference for functions. (Contributed by AV, 7-Feb-2021.)
⊢ 𝐹 = 𝐺    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)
Theorem	feq23i 5952	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷)
Theorem	feq23d 5953	Equality deduction for functions. (Contributed by NM, 8-Jun-2013.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))
Theorem	nff 5954	Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴⟶𝐵
Theorem	sbcfng 5955*	Distribute proper substitution through the function predicate with a domain. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ (𝑋 ∈ 𝑉 → ([𝑋 / 𝑥]𝐹 Fn 𝐴 ↔ ⦋𝑋 / 𝑥⦌𝐹 Fn ⦋𝑋 / 𝑥⦌𝐴))
Theorem	sbcfg 5956*	Distribute proper substitution through the function predicate with domain and codomain. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ (𝑋 ∈ 𝑉 → ([𝑋 / 𝑥]𝐹:𝐴⟶𝐵 ↔ ⦋𝑋 / 𝑥⦌𝐹:⦋𝑋 / 𝑥⦌𝐴⟶⦋𝑋 / 𝑥⦌𝐵))
Theorem	elimf 5957	Eliminate a mapping hypothesis for the weak deduction theorem dedth 4089, when a special case 𝐺:𝐴⟶𝐵 is provable, in order to convert 𝐹:𝐴⟶𝐵 from a hypothesis to an antecedent. (Contributed by NM, 24-Aug-2006.)
⊢ 𝐺:𝐴⟶𝐵    ⇒   ⊢ if(𝐹:𝐴⟶𝐵, 𝐹, 𝐺):𝐴⟶𝐵
Theorem	ffn 5958	A mapping is a function with domain. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
Theorem	ffnd 5959	A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 Fn 𝐴)
Theorem	dffn2 5960	Any function is a mapping into V. (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)
Theorem	ffun 5961	A mapping is a function. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
Theorem	ffund 5962	A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	frel 5963	A mapping is a relation. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)
Theorem	fdm 5964	The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
Theorem	fdmi 5965	The domain of a mapping. (Contributed by NM, 28-Jul-2008.)
⊢ 𝐹:𝐴⟶𝐵    ⇒   ⊢ dom 𝐹 = 𝐴
Theorem	frn 5966	The range of a mapping. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
Theorem	dffn3 5967	A function maps to its range. (Contributed by NM, 1-Sep-1999.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)
Theorem	ffrn 5968	A function maps to its range. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶ran 𝐹)
Theorem	fss 5969	Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
Theorem	fssd 5970	Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fco 5971	Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
Theorem	fco2 5972	Functionality of a composition with weakened out of domain condition on the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ (((𝐹 ↾ 𝐵):𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
Theorem	fssxp 5973	A mapping is a class of ordered pairs. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
Theorem	funssxp 5974	Two ways of specifying a partial function from 𝐴 to 𝐵. (Contributed by NM, 13-Nov-2007.)
⊢ ((Fun 𝐹 ∧ 𝐹 ⊆ (𝐴 × 𝐵)) ↔ (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
Theorem	ffdm 5975	A mapping is a partial function. (Contributed by NM, 25-Nov-2007.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
Theorem	ffdmd 5976	The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵)
Theorem	fdmrn 5977	A different way to write 𝐹 is a function. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ (Fun 𝐹 ↔ 𝐹:dom 𝐹⟶ran 𝐹)
Theorem	opelf 5978	The members of an ordered pair element of a mapping belong to the mapping's domain and codomain. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ ⟨𝐶, 𝐷⟩ ∈ 𝐹) → (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵))
Theorem	fun 5979	The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)
⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷))
Theorem	fun2 5980	The union of two functions with disjoint domains. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶)
Theorem	fun2d 5981	The union of functions with disjoint domains is a function, deduction version of fun2 5980. (Contributed by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶)
Theorem	fnfco 5982	Composition of two functions. (Contributed by NM, 22-May-2006.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺:𝐵⟶𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵)
Theorem	fssres 5983	Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
Theorem	fssresd 5984	Restriction of a function with a subclass of its domain, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
Theorem	fssres2 5985	Restriction of a restricted function with a subclass of its domain. (Contributed by NM, 21-Jul-2005.)
⊢ (((𝐹 ↾ 𝐴):𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
Theorem	fresin 5986	An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ 𝑋):(𝐴 ∩ 𝑋)⟶𝐵)
Theorem	resasplit 5987	If two functions agree on their common domain, express their union as a union of three functions with pairwise disjoint domains. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))))
Theorem	fresaun 5988	The union of two functions which agree on their common domain is a function. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶)
Theorem	fresaunres2 5989	From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Stefan O'Rear, 9-Oct-2014.)
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺)
Theorem	fresaunres1 5990	From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐴) = 𝐹)
Theorem	fcoi1 5991	Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
Theorem	fcoi2 5992	Composition of restricted identity and a mapping. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
Theorem	feu 5993*	There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ∃!𝑦 ∈ 𝐵 ⟨𝐶, 𝑦⟩ ∈ 𝐹)
Theorem	fimass 5994	The image of a class is a subset of its codomain. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 “ 𝑋) ⊆ 𝐵)
Theorem	fcnvres 5995	The converse of a restriction of a function. (Contributed by NM, 26-Mar-1998.)
⊢ (𝐹:𝐴⟶𝐵 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ 𝐵))
Theorem	fimacnvdisj 5996	The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (◡𝐹 “ 𝐶) = ∅)
Theorem	fint 5997*	Function into an intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ 𝐵 ≠ ∅    ⇒   ⊢ (𝐹:𝐴⟶∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐹:𝐴⟶𝑥)
Theorem	fin 5998	Mapping into an intersection. (Contributed by NM, 14-Sep-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶(𝐵 ∩ 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴⟶𝐶))
Theorem	f0 5999	The empty function. (Contributed by NM, 14-Aug-1999.)
⊢ ∅:∅⟶𝐴
Theorem	f00 6000	A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003.)
⊢ (𝐹:𝐴⟶∅ ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))