P. 70 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6901-7000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fveqeq2 6901	Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.)
⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))
Theorem	nffv 6902	Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹‘𝐴)
Theorem	nffvmpt1 6903*	Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶)
Theorem	nffvd 6904	Deduction version of bound-variable hypothesis builder nffv 6902. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐹‘𝐴))
Theorem	fvex 6905	The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by NM, 30-Dec-1996.)
⊢ (𝐹‘𝐴) ∈ V
Theorem	fvexi 6906	The value of a class exists. Inference form of fvex 6905. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝐴 = (𝐹‘𝐵)    ⇒   ⊢ 𝐴 ∈ V
Theorem	fvexd 6907	The value of a class exists (as consequent of anything). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → (𝐹‘𝐴) ∈ V)
Theorem	fvif 6908	Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐹‘if(𝜑, 𝐴, 𝐵)) = if(𝜑, (𝐹‘𝐴), (𝐹‘𝐵))
Theorem	iffv 6909	Move a conditional outside of a function. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (if(𝜑, 𝐹, 𝐺)‘𝐴) = if(𝜑, (𝐹‘𝐴), (𝐺‘𝐴))
Theorem	fv3 6910*	Alternate definition of the value of a function. Definition 6.11 of [TakeutiZaring] p. 26. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐹‘𝐴) = {𝑥 ∣ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝐴𝐹𝑦) ∧ ∃!𝑦 𝐴𝐹𝑦)}
Theorem	fvres 6911	The value of a restricted function. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))
Theorem	fvresd 6912	The value of a restricted function, deduction version of fvres 6911. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))
Theorem	funssfv 6913	The value of a member of the domain of a subclass of a function. (Contributed by NM, 15-Aug-1994.)
⊢ ((Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ∈ dom 𝐺) → (𝐹‘𝐴) = (𝐺‘𝐴))
Theorem	tz6.12c 6914*	Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.) (Proof shortened by SN, 23-Dec-2024.)
⊢ (∃!𝑦 𝐴𝐹𝑦 → ((𝐹‘𝐴) = 𝑦 ↔ 𝐴𝐹𝑦))
Theorem	tz6.12-1 6915*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.) (Proof shortened by SN, 23-Dec-2024.)
⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹‘𝐴) = 𝑦)
Theorem	tz6.12-1OLD 6916*	Obsolete version of tz6.12-1 6915 as of 23-Dec-2024. (Contributed by NM, 30-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹‘𝐴) = 𝑦)
Theorem	tz6.12 6917*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 10-Jul-1994.)
⊢ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹‘𝐴) = 𝑦)
Theorem	tz6.12f 6918*	Function value, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 30-Aug-1999.)
⊢ Ⅎ𝑦𝐹    ⇒   ⊢ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹‘𝐴) = 𝑦)
Theorem	tz6.12cOLD 6919*	Obsolete version of tz6.12c 6914 as of 23-Dec-2024. (Contributed by NM, 30-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃!𝑦 𝐴𝐹𝑦 → ((𝐹‘𝐴) = 𝑦 ↔ 𝐴𝐹𝑦))
Theorem	tz6.12i 6920	Corollary of Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐵 ≠ ∅ → ((𝐹‘𝐴) = 𝐵 → 𝐴𝐹𝐵))
Theorem	fvbr0 6921	Two possibilities for the behavior of a function value. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑋𝐹(𝐹‘𝑋) ∨ (𝐹‘𝑋) = ∅)
Theorem	fvrn0 6922	A function value is a member of the range plus null. (Contributed by Scott Fenton, 8-Jun-2011.) (Revised by Stefan O'Rear, 3-Jan-2015.)
⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅})
Theorem	fvn0fvelrn 6923	If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Proof shortened by SN, 13-Jan-2025.)
⊢ ((𝐹‘𝑋) ≠ ∅ → (𝐹‘𝑋) ∈ ran 𝐹)
Theorem	elfvunirn 6924	A function value is a subset of the union of the range. (An artifact of our function value definition, compare elfvdm 6929). (Contributed by Thierry Arnoux, 13-Nov-2016.) Remove functionhood antecedent. (Revised by SN, 10-Jan-2025.)
⊢ (𝐵 ∈ (𝐹‘𝐴) → 𝐵 ∈ ∪ ran 𝐹)
Theorem	fvssunirn 6925	The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof shortened by SN, 13-Jan-2025.)
⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹
Theorem	fvssunirnOLD 6926	Obsolete version of fvssunirn 6925 as of 13-Jan-2025. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹
Theorem	ndmfv 6927	The value of a class outside its domain is the empty set. (An artifact of our function value definition.) (Contributed by NM, 24-Aug-1995.)
⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)
Theorem	ndmfvrcl 6928	Reverse closure law for function with the empty set not in its domain. (Contributed by NM, 26-Apr-1996.)
⊢ dom 𝐹 = 𝑆    &   ⊢ ¬ ∅ ∈ 𝑆    ⇒   ⊢ ((𝐹‘𝐴) ∈ 𝑆 → 𝐴 ∈ 𝑆)
Theorem	elfvdm 6929	If a function value has a member, then the argument belongs to the domain. (An artifact of our function value definition.) (Contributed by NM, 12-Feb-2007.) (Proof shortened by BJ, 22-Oct-2022.)
⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)
Theorem	elfvex 6930	If a function value has a member, then the argument is a set. (An artifact of our function value definition.) (Contributed by Mario Carneiro, 6-Nov-2015.)
⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V)
Theorem	elfvexd 6931	If a function value has a member, then its argument is a set. Deduction form of elfvex 6930. (An artifact of our function value definition.) (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵‘𝐶))    ⇒   ⊢ (𝜑 → 𝐶 ∈ V)
Theorem	eliman0 6932	A nonempty function value is an element of the image of the function. (Contributed by Thierry Arnoux, 25-Jun-2019.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ (𝐹‘𝐴) = ∅) → (𝐹‘𝐴) ∈ (𝐹 “ 𝐵))
Theorem	nfvres 6933	The value of a non-member of a restriction is the empty set. (An artifact of our function value definition.) (Contributed by NM, 13-Nov-1995.)
⊢ (¬ 𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = ∅)
Theorem	nfunsn 6934	If the restriction of a class to a singleton is not a function, then its value is the empty set. (An artifact of our function value definition.) (Contributed by NM, 8-Aug-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹‘𝐴) = ∅)
Theorem	fvfundmfvn0 6935	If the "value of a class" at an argument is not the empty set, then the argument is in the domain of the class and the class restricted to the singleton formed on that argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.) (Proof shortened by BJ, 13-Aug-2022.)
⊢ ((𝐹‘𝐴) ≠ ∅ → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
Theorem	0fv 6936	Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.)
⊢ (∅‘𝐴) = ∅
Theorem	fv2prc 6937	A function value of a function value at a proper class is the empty set. (Contributed by AV, 8-Apr-2021.)
⊢ (¬ 𝐴 ∈ V → ((𝐹‘𝐴)‘𝐵) = ∅)
Theorem	elfv2ex 6938	If a function value of a function value has a member, then the first argument is a set. (Contributed by AV, 8-Apr-2021.)
⊢ (𝐴 ∈ ((𝐹‘𝐵)‘𝐶) → 𝐵 ∈ V)
Theorem	fveqres 6939	Equal values imply equal values in a restriction. (Contributed by NM, 13-Nov-1995.)
⊢ ((𝐹‘𝐴) = (𝐺‘𝐴) → ((𝐹 ↾ 𝐵)‘𝐴) = ((𝐺 ↾ 𝐵)‘𝐴))
Theorem	csbfv12 6940	Move class substitution in and out of a function value. (Contributed by NM, 11-Nov-2005.) (Revised by NM, 20-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵)
Theorem	csbfv2g 6941*	Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (𝐹‘⦋𝐴 / 𝑥⦌𝐵))
Theorem	csbfv 6942*	Substitution for a function value. (Contributed by NM, 1-Jan-2006.) (Revised by NM, 20-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘𝐴)
Theorem	funbrfv 6943	The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹‘𝐴) = 𝐵))
Theorem	funopfv 6944	The second element in an ordered pair member of a function is the function's value. (Contributed by NM, 19-Jul-1996.)
⊢ (Fun 𝐹 → (⟨𝐴, 𝐵⟩ ∈ 𝐹 → (𝐹‘𝐴) = 𝐵))
Theorem	fnbrfvb 6945	Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ 𝐵𝐹𝐶))
Theorem	fnopfvb 6946	Equivalence of function value and ordered pair membership. (Contributed by NM, 7-Nov-1995.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐹))
Theorem	funbrfvb 6947	Equivalence of function value and binary relation. (Contributed by NM, 26-Mar-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) = 𝐵 ↔ 𝐴𝐹𝐵))
Theorem	funopfvb 6948	Equivalence of function value and ordered pair membership. Theorem 4.3(ii) of [Monk1] p. 42. (Contributed by NM, 26-Jan-1997.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) = 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐹))
Theorem	fnbrfvb2 6949	Version of fnbrfvb 6945 for functions on Cartesian products: function value expressed as a binary relation. See fnbrovb 7464 for the form when 𝐹 is seen as a binary operation. (Contributed by BJ, 15-Feb-2022.)
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((𝐹‘⟨𝐴, 𝐵⟩) = 𝐶 ↔ ⟨𝐴, 𝐵⟩𝐹𝐶))
Theorem	fdmeu 6950*	There is exactly one codomain element for each element of the domain of a function. (Contributed by AV, 20-Apr-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ 𝐴) → ∃!𝑦 ∈ 𝐵 (𝐹‘𝑋) = 𝑦)
Theorem	funbrfv2b 6951	Function value in terms of a binary relation. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ (𝐹‘𝐴) = 𝐵)))
Theorem	dffn5 6952*	Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
Theorem	fnrnfv 6953*	The range of a function expressed as a collection of the function's values. (Contributed by NM, 20-Oct-2005.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
Theorem	fvelrnb 6954*	A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995.)
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
Theorem	foelcdmi 6955*	A member of a surjective function's codomain is a value of the function. (Contributed by Thierry Arnoux, 23-Jan-2020.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑌)
Theorem	dfimafn 6956*	Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦})
Theorem	dfimafn2 6957*	Alternate definition of the image of a function as an indexed union of singletons of function values. (Contributed by Raph Levien, 20-Nov-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = ∪ 𝑥 ∈ 𝐴 {(𝐹‘𝑥)})
Theorem	funimass4 6958*	Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	fvelima 6959*	Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42. (Contributed by NM, 29-Apr-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴)
Theorem	funimassd 6960*	Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐵)
Theorem	fvelimad 6961*	Function value in an image. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐹 “ 𝐵))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑥) = 𝐶)
Theorem	feqmptd 6962*	Deduction form of dffn5 6952. (Contributed by Mario Carneiro, 8-Jan-2015.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
Theorem	feqresmpt 6963*	Express a restricted function as a mapping. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
Theorem	feqmptdf 6964	Deduction form of dffn5f 6965. (Contributed by Mario Carneiro, 8-Jan-2015.) (Revised by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
Theorem	dffn5f 6965*	Representation of a function in terms of its values. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
Theorem	fvelimab 6966*	Function value in an image. (Contributed by NM, 20-Jan-2007.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by David Abernethy, 17-Dec-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))
Theorem	fvelimabd 6967*	Deduction form of fvelimab 6966. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))
Theorem	unima 6968	Image of a union. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 “ (𝐵 ∪ 𝐶)) = ((𝐹 “ 𝐵) ∪ (𝐹 “ 𝐶)))
Theorem	fvi 6969	The value of the identity function. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → ( I ‘𝐴) = 𝐴)
Theorem	fviss 6970	The value of the identity function is a subset of the argument. (An artifact of our function value definition.) (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ ( I ‘𝐴) ⊆ 𝐴
Theorem	fniinfv 6971*	The indexed intersection of a function's values is the intersection of its range. (Contributed by NM, 20-Oct-2005.)
⊢ (𝐹 Fn 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∩ ran 𝐹)
Theorem	fnsnfv 6972	Singleton of function value. (Contributed by NM, 22-May-1998.) (Proof shortened by Scott Fenton, 8-Aug-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵}))
Theorem	fnsnfvOLD 6973	Obsolete version of fnsnfv 6972 as of 8-Aug-2024. (Contributed by NM, 22-May-1998.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵}))
Theorem	opabiotafun 6974*	Define a function whose value is "the unique 𝑦 such that 𝜑(𝑥, 𝑦)". (Contributed by NM, 19-May-2015.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ {𝑦 ∣ 𝜑} = {𝑦}}    ⇒   ⊢ Fun 𝐹
Theorem	opabiotadm 6975*	Define a function whose value is "the unique 𝑦 such that 𝜑(𝑥, 𝑦)". (Contributed by NM, 16-Nov-2013.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ {𝑦 ∣ 𝜑} = {𝑦}}    ⇒   ⊢ dom 𝐹 = {𝑥 ∣ ∃!𝑦𝜑}
Theorem	opabiota 6976*	Define a function whose value is "the unique 𝑦 such that 𝜑(𝑥, 𝑦)". (Contributed by NM, 16-Nov-2013.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ {𝑦 ∣ 𝜑} = {𝑦}}    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = (℩𝑦𝜓))
Theorem	fnimapr 6977	The image of a pair under a function. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹 “ {𝐵, 𝐶}) = {(𝐹‘𝐵), (𝐹‘𝐶)})
Theorem	ssimaex 6978*	The existence of a subimage. (Contributed by NM, 8-Apr-2007.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ 𝐴)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))
Theorem	ssimaexg 6979*	The existence of a subimage. (Contributed by FL, 15-Apr-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ 𝐴)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))
Theorem	funfv 6980	A simplified expression for the value of a function when we know it is a function. (Contributed by NM, 22-May-1998.)
⊢ (Fun 𝐹 → (𝐹‘𝐴) = ∪ (𝐹 “ {𝐴}))
Theorem	funfv2 6981*	The value of a function. Definition of function value in [Enderton] p. 43. (Contributed by NM, 22-May-1998.)
⊢ (Fun 𝐹 → (𝐹‘𝐴) = ∪ {𝑦 ∣ 𝐴𝐹𝑦})
Theorem	funfv2f 6982	The value of a function. Version of funfv2 6981 using a bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 19-Feb-2006.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐹    ⇒   ⊢ (Fun 𝐹 → (𝐹‘𝐴) = ∪ {𝑦 ∣ 𝐴𝐹𝑦})
Theorem	fvun 6983	Value of the union of two functions when the domains are separate. (Contributed by FL, 7-Nov-2011.)
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹 ∪ 𝐺)‘𝐴) = ((𝐹‘𝐴) ∪ (𝐺‘𝐴)))
Theorem	fvun1 6984	The value of a union when the argument is in the first domain. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋))
Theorem	fvun2 6985	The value of a union when the argument is in the second domain. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐵)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐺‘𝑋))
Theorem	fvun1d 6986	The value of a union when the argument is in the first domain, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋))
Theorem	fvun2d 6987	The value of a union when the argument is in the second domain, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐺‘𝑋))
Theorem	dffv2 6988	Alternate definition of function value df-fv 6551 that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010.)
⊢ (𝐹‘𝐴) = ∪ ((𝐹 “ {𝐴}) ∖ ∪ ∪ (((𝐹 ↾ {𝐴}) ∘ ◡(𝐹 ↾ {𝐴})) ∖ I ))
Theorem	dmfco 6989	Domains of a function composition. (Contributed by NM, 27-Jan-1997.)
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝐴) ∈ dom 𝐹))
Theorem	fvco2 6990	Value of a function composition. Similar to second part of Theorem 3H of [Enderton] p. 47. (Contributed by NM, 9-Oct-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 16-Oct-2014.)
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)))
Theorem	fvco 6991	Value of a function composition. Similar to Exercise 5 of [TakeutiZaring] p. 28. (Contributed by NM, 22-Apr-2006.) (Proof shortened by Mario Carneiro, 26-Dec-2014.)
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐹 ∘ 𝐺)‘𝐴) = (𝐹‘(𝐺‘𝐴)))
Theorem	fvco3 6992	Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.)
⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
Theorem	fvco3d 6993	Value of a function composition. Deduction form of fvco3 6992. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
Theorem	fvco4i 6994	Conditions for a composition to be expandable without conditions on the argument. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ ∅ = (𝐹‘∅)    &   ⊢ Fun 𝐺    ⇒   ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋))
Theorem	fvopab3g 6995*	Value of a function given by ordered-pair class abstraction. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦𝜑)    &   ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((𝐹‘𝐴) = 𝐵 ↔ 𝜒))
Theorem	fvopab3ig 6996*	Value of a function given by ordered-pair class abstraction. (Contributed by NM, 23-Oct-1999.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 ∈ 𝐶 → ∃*𝑦𝜑)    &   ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝜒 → (𝐹‘𝐴) = 𝐵))
Theorem	brfvopabrbr 6997*	The binary relation of a function value which is an ordered-pair class abstraction of a restricted binary relation is the restricted binary relation. The first hypothesis can often be obtained by using fvmptopab 7469. (Contributed by AV, 29-Oct-2021.)
⊢ (𝐴‘𝑍) = {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝐵‘𝑍)𝑦 ∧ 𝜑)}    &   ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓))    &   ⊢ Rel (𝐵‘𝑍)    ⇒   ⊢ (𝑋(𝐴‘𝑍)𝑌 ↔ (𝑋(𝐵‘𝑍)𝑌 ∧ 𝜓))
Theorem	fvmptg 6998*	Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)
Theorem	fvmpti 6999*	Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    ⇒   ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = ( I ‘𝐶))
Theorem	fvmpt 7000*	Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)