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	tz6.12-2 6901*	Function value when 𝐹 is not a function. Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) Avoid ax-10 2180, ax-11 2197, ax-12 2216. (Revised by TM, 25-Jan-2026.)
⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
Theorem	tz6.12-2OLD 6902*	Obsolete version of tz6.12-2 6901 as of 25-Jan-2026. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
Theorem	fveu 6903*	The value of a function at a unique point. (Contributed by Scott Fenton, 6-Oct-2017.)
⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})
Theorem	brprcneu 6904*	If 𝐴 is a proper class and 𝐹 is any class, then there is no unique set which is related to 𝐴 through the binary relation 𝐹. See brprcneuALT 6905 for a proof that uses ax-pow 5332 instead of ax-pr 5396. (Contributed by Scott Fenton, 7-Oct-2017.)
⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
Theorem	brprcneuALT 6905*	Alternate proof of brprcneu 6904 using ax-pow 5332 instead of ax-pr 5396. (Contributed by Scott Fenton, 7-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
Theorem	fvprc 6906	A function's value at a proper class is the empty set. See fvprcALT 6907 for a proof that uses ax-pow 5332 instead of ax-pr 5396. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5332. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.)
⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
Theorem	fvprcALT 6907	Alternate proof of fvprc 6906 using ax-pow 5332 instead of ax-pr 5396. (Contributed by NM, 20-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
Theorem	rnfvprc 6908	The range of a function value at a proper class is empty. (Contributed by AV, 20-Aug-2022.)
⊢ 𝑌 = (𝐹‘𝑋)    ⇒   ⊢ (¬ 𝑋 ∈ V → ran 𝑌 = ∅)
Theorem	fv2 6909*	Alternate definition of function value. Definition 10.11 of [Quine] p. 68. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐹‘𝐴) = ∪ {𝑥 ∣ ∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥)}
Theorem	dffv3 6910*	A definition of function value in terms of iota. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐹‘𝐴) = (℩𝑥𝑥 ∈ (𝐹 “ {𝐴}))
Theorem	dffv4 6911*	The previous definition of function value, from before the ℩ operator was introduced. Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 6106), this definition apparently does not appear in the literature. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹‘𝐴) = ∪ {𝑥 ∣ (𝐹 “ {𝐴}) = {𝑥}}
Theorem	elfv 6912*	Membership in a function value. (Contributed by NM, 30-Apr-2004.)
⊢ (𝐴 ∈ (𝐹‘𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)))
Theorem	fveq1 6913	Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
Theorem	fveq2 6914	Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
Theorem	fveq1i 6915	Equality inference for function value. (Contributed by NM, 2-Sep-2003.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)
Theorem	fveq1d 6916	Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))
Theorem	fveq2i 6917	Equality inference for function value. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)
Theorem	fveq2d 6918	Equality deduction for function value. (Contributed by NM, 29-May-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))
Theorem	2fveq3 6919	Equality theorem for nested function values. (Contributed by AV, 14-Aug-2022.)
⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵)))
Theorem	fveq12i 6920	Equality deduction for function value. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐹 = 𝐺    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹‘𝐴) = (𝐺‘𝐵)
Theorem	fveq12d 6921	Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))
Theorem	fveqeq2d 6922	Equality deduction for function value. (Contributed by BJ, 30-Aug-2022.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))
Theorem	fveqeq2 6923	Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.)
⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))
Theorem	nffv 6924	Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹‘𝐴)
Theorem	nffvmpt1 6925*	Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶)
Theorem	nffvd 6926	Deduction version of bound-variable hypothesis builder nffv 6924. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐹‘𝐴))
Theorem	fvex 6927	The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by NM, 30-Dec-1996.)
⊢ (𝐹‘𝐴) ∈ V
Theorem	fvexi 6928	The value of a class exists. Inference form of fvex 6927. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝐴 = (𝐹‘𝐵)    ⇒   ⊢ 𝐴 ∈ V
Theorem	fvexd 6929	The value of a class exists (as consequent of anything). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → (𝐹‘𝐴) ∈ V)
Theorem	fvif 6930	Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐹‘if(𝜑, 𝐴, 𝐵)) = if(𝜑, (𝐹‘𝐴), (𝐹‘𝐵))
Theorem	iffv 6931	Move a conditional outside of a function. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (if(𝜑, 𝐹, 𝐺)‘𝐴) = if(𝜑, (𝐹‘𝐴), (𝐺‘𝐴))
Theorem	fv3 6932*	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 6933	The value of a restricted function. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))
Theorem	fvresd 6934	The value of a restricted function, deduction version of fvres 6933. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))
Theorem	funssfv 6935	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 6936*	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 6937*	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 6938*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 10-Jul-1994.)
⊢ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹‘𝐴) = 𝑦)
Theorem	tz6.12f 6939*	Function value, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 30-Aug-1999.)
⊢ Ⅎ𝑦𝐹    ⇒   ⊢ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹‘𝐴) = 𝑦)
Theorem	tz6.12i 6940	Corollary of Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐵 ≠ ∅ → ((𝐹‘𝐴) = 𝐵 → 𝐴𝐹𝐵))
Theorem	fvbr0 6941	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 6942	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 6943	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 6944	A function value is a subset of the union of the range. (An artifact of our function value definition, compare elfvdm 6948). (Contributed by Thierry Arnoux, 13-Nov-2016.) Remove functionhood antecedent. (Revised by SN, 10-Jan-2025.)
⊢ (𝐵 ∈ (𝐹‘𝐴) → 𝐵 ∈ ∪ ran 𝐹)
Theorem	fvssunirn 6945	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	ndmfv 6946	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 6947	Reverse closure law for function with the empty set not in its domain (if 𝑅 = 𝑆). (Contributed by NM, 26-Apr-1996.) The class containing the function value does not have to be the domain. (Revised by Zhi Wang, 10-Nov-2025.)
⊢ dom 𝐹 = 𝑆    &   ⊢ ¬ ∅ ∈ 𝑅    ⇒   ⊢ ((𝐹‘𝐴) ∈ 𝑅 → 𝐴 ∈ 𝑆)
Theorem	elfvdm 6948	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 6949	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 6950	If a function value has a member, then its argument is a set. Deduction form of elfvex 6949. (An artifact of our function value definition.) (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (𝐵‘𝐶))    ⇒   ⊢ (𝜑 → 𝐶 ∈ V)
Theorem	eliman0 6951	A nonempty function value is an element of the image of the function. (Contributed by Thierry Arnoux, 25-Jun-2019.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ (𝐹‘𝐴) = ∅) → (𝐹‘𝐴) ∈ (𝐹 “ 𝐵))
Theorem	nfvres 6952	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 6953	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 6954	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 6955	Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.)
⊢ (∅‘𝐴) = ∅
Theorem	fv2prc 6956	A function value of a function value at a proper class is the empty set. (Contributed by AV, 8-Apr-2021.)
⊢ (¬ 𝐴 ∈ V → ((𝐹‘𝐴)‘𝐵) = ∅)
Theorem	elfv2ex 6957	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 6958	Equal values imply equal values in a restriction. (Contributed by NM, 13-Nov-1995.)
⊢ ((𝐹‘𝐴) = (𝐺‘𝐴) → ((𝐹 ↾ 𝐵)‘𝐴) = ((𝐺 ↾ 𝐵)‘𝐴))
Theorem	csbfv12 6959	Move class substitution in and out of a function value. (Contributed by NM, 11-Nov-2005.) (Revised by NM, 20-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵)
Theorem	csbfv2g 6960*	Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (𝐹‘⦋𝐴 / 𝑥⦌𝐵))
Theorem	csbfv 6961*	Substitution for a function value. (Contributed by NM, 1-Jan-2006.) (Revised by NM, 20-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐹‘𝑥) = (𝐹‘𝐴)
Theorem	funbrfv 6962	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 6963	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 6964	Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ 𝐵𝐹𝐶))
Theorem	fnopfvb 6965	Equivalence of function value and ordered pair membership. (Contributed by NM, 7-Nov-1995.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐹))
Theorem	fvelima2 6966*	Function value in an image. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (𝐹 “ 𝐶)) → ∃𝑥 ∈ (𝐴 ∩ 𝐶)(𝐹‘𝑥) = 𝐵)
Theorem	funbrfvb 6967	Equivalence of function value and binary relation. (Contributed by NM, 26-Mar-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) = 𝐵 ↔ 𝐴𝐹𝐵))
Theorem	funopfvb 6968	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 6969	Version of fnbrfvb 6964 for functions on Cartesian products: function value expressed as a binary relation. See fnbrovb 7500 for the form when 𝐹 is seen as a binary operation. (Contributed by BJ, 15-Feb-2022.)
⊢ ((𝐹 Fn (𝑉 × 𝑊) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((𝐹‘⟨𝐴, 𝐵⟩) = 𝐶 ↔ ⟨𝐴, 𝐵⟩𝐹𝐶))
Theorem	fdmeu 6970*	There is exactly one codomain element for each element of the domain of a function. (Contributed by AV, 20-Apr-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ 𝐴) → ∃!𝑦 ∈ 𝐵 (𝐹‘𝑋) = 𝑦)
Theorem	funbrfv2b 6971	Function value in terms of a binary relation. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ (𝐹‘𝐴) = 𝐵)))
Theorem	dffn5 6972*	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 6973*	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 6974*	A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995.)
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
Theorem	foelcdmi 6975*	A member of a surjective function's codomain is a value of the function. (Contributed by Thierry Arnoux, 23-Jan-2020.)
⊢ ((𝐹:𝐴⟶onto𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑌)
Theorem	dfimafn 6976*	Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦})
Theorem	dfimafn2 6977*	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 6978*	Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	fvelima 6979*	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 6980*	Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐵)
Theorem	fvelimad 6981*	Function value in an image. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐹 “ 𝐵))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑥) = 𝐶)
Theorem	feqmptd 6982*	Deduction form of dffn5 6972. (Contributed by Mario Carneiro, 8-Jan-2015.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
Theorem	feqresmpt 6983*	Express a restricted function as a mapping. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
Theorem	feqmptdf 6984	Deduction form of dffn5f 6985. (Contributed by Mario Carneiro, 8-Jan-2015.) (Revised by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
Theorem	dffn5f 6985*	Representation of a function in terms of its values. (Contributed by Mario Carneiro, 3-Jul-2015.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
Theorem	fvelimab 6986*	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 6987*	Deduction form of fvelimab 6986. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))
Theorem	fimarab 6988*	Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝐹 “ 𝑋) = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑦})
Theorem	unima 6989	Image of a union. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 “ (𝐵 ∪ 𝐶)) = ((𝐹 “ 𝐵) ∪ (𝐹 “ 𝐶)))
Theorem	fvi 6990	The value of the identity function. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → ( I ‘𝐴) = 𝐴)
Theorem	fviss 6991	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 6992*	The indexed intersection of a function's values is the intersection of its range. (Contributed by NM, 20-Oct-2005.)
⊢ (𝐹 Fn 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∩ ran 𝐹)
Theorem	fnsnfv 6993	Singleton of function value. (Contributed by NM, 22-May-1998.) (Proof shortened by Scott Fenton, 8-Aug-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵}))
Theorem	opabiotafun 6994*	Define a function whose value is "the unique 𝑦 such that 𝜑(𝑥, 𝑦)". (Contributed by NM, 19-May-2015.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ {𝑦 ∣ 𝜑} = {𝑦}}    ⇒   ⊢ Fun 𝐹
Theorem	opabiotadm 6995*	Define a function whose value is "the unique 𝑦 such that 𝜑(𝑥, 𝑦)". (Contributed by NM, 16-Nov-2013.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ {𝑦 ∣ 𝜑} = {𝑦}}    ⇒   ⊢ dom 𝐹 = {𝑥 ∣ ∃!𝑦𝜑}
Theorem	opabiota 6996*	Define a function whose value is "the unique 𝑦 such that 𝜑(𝑥, 𝑦)". (Contributed by NM, 16-Nov-2013.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ {𝑦 ∣ 𝜑} = {𝑦}}    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = (℩𝑦𝜓))
Theorem	fnimapr 6997	The image of a pair under a function. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹 “ {𝐵, 𝐶}) = {(𝐹‘𝐵), (𝐹‘𝐶)})
Theorem	fnimatpd 6998	The image of an unordered triple under a function. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 “ {𝐴, 𝐵, 𝐶}) = {(𝐹‘𝐴), (𝐹‘𝐵), (𝐹‘𝐶)})
Theorem	ssimaex 6999*	The existence of a subimage. (Contributed by NM, 8-Apr-2007.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ 𝐴)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))
Theorem	ssimaexg 7000*	The existence of a subimage. (Contributed by FL, 15-Apr-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ 𝐴)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))