P. 64 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6301-6400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ffvresb 6301*	A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (Fun 𝐹 → ((𝐹 ↾ 𝐴):𝐴⟶𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐵)))
Theorem	f1oresrab 6302*	Build a bijection between restricted abstract builders, given a bijection between the base classes, deduction version. (Contributed by Thierry Arnoux, 17-Aug-2018.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) → (𝜒 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒})
Theorem	fmptco 6303*	Composition of two functions expressed as ordered-pair class abstractions. If 𝐹 has the equation (𝑥 + 2) and 𝐺 the equation (3∗𝑧) then (𝐺 ∘ 𝐹) has the equation (3∗(𝑥 + 2)). (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))
Theorem	fmptcof 6304*	Version of fmptco 6303 where 𝜑 needn't be distinct from 𝑥. (Contributed by NM, 27-Dec-2014.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))
Theorem	fmptcos 6305*	Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ ⦋𝑅 / 𝑦⦌𝑆))
Theorem	fcompt 6306*	Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥))))
Theorem	fcoconst 6307	Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)}))
Theorem	fsn 6308	A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {⟨𝐴, 𝐵⟩})
Theorem	fsn2 6309	A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹:{𝐴}⟶𝐵 ↔ ((𝐹‘𝐴) ∈ 𝐵 ∧ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩}))
Theorem	fsng 6310	A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {⟨𝐴, 𝐵⟩}))
Theorem	fsn2g 6311	A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by Thierry Arnoux, 11-Jul-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐹:{𝐴}⟶𝐵 ↔ ((𝐹‘𝐴) ∈ 𝐵 ∧ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})))
Theorem	xpsng 6312	The Cartesian product of two singletons. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩})
Theorem	xpsn 6313	The Cartesian product of two singletons. (Contributed by NM, 4-Nov-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩}
Theorem	f1o2sn 6314	A singleton with a nested ordered pair is a 1-1 function of the cartesian product of two singleton onto a singleton. (Contributed by AV, 15-Aug-2019.)
⊢ ((𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → {⟨⟨𝐸, 𝐸⟩, 𝑋⟩}:({𝐸} × {𝐸})–1-1-onto→{𝑋})
Theorem	residpr 6315	Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( I ↾ {𝐴, 𝐵}) = {⟨𝐴, 𝐴⟩, ⟨𝐵, 𝐵⟩})
Theorem	dfmpt 6316	Alternate definition for the "maps to" notation df-mpt 4645 (although it requires that 𝐵 be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
Theorem	fnasrn 6317	A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ran (𝑥 ∈ 𝐴 ↦ ⟨𝑥, 𝐵⟩)
Theorem	funiun 6318*	A function is a union of singletons of ordered pairs indexed by its domain. (Contributed by AV, 18-Sep-2020.)
⊢ (Fun 𝐹 → 𝐹 = ∪ 𝑥 ∈ dom 𝐹{⟨𝑥, (𝐹‘𝑥)⟩})
Theorem	funopsn 6319*	If a function is an ordered pair then it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐹 = ⟨𝑋, 𝑌⟩) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {⟨𝑎, 𝑎⟩}))
Theorem	funop 6320*	An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    ⇒   ⊢ (Fun ⟨𝑋, 𝑌⟩ ↔ ∃𝑎(𝑋 = {𝑎} ∧ ⟨𝑋, 𝑌⟩ = {⟨𝑎, 𝑎⟩}))
Theorem	funsndifnop 6321	A singleton of an ordered pair is not an ordered pair if the components are different. (Contributed by AV, 23-Sep-2020.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = {⟨𝐴, 𝐵⟩}    ⇒   ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐺 ∈ (V × V))
Theorem	funsneqopsn 6322	A singleton of an ordered pair is an ordered pair of equal singletons if the components are equal. (Contributed by AV, 24-Sep-2020.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = {⟨𝐴, 𝐵⟩}    ⇒   ⊢ (𝐴 = 𝐵 → 𝐺 = ⟨{𝐴}, {𝐴}⟩)
Theorem	funsneqop 6323	A singleton of an ordered pair is an ordered pair if the components are equal. (Contributed by AV, 24-Sep-2020.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = {⟨𝐴, 𝐵⟩}    ⇒   ⊢ (𝐴 = 𝐵 → 𝐺 ∈ (V × V))
Theorem	funsneqopb 6324	A singleton of an ordered pair is an ordered pair iff the components are equal. (Contributed by AV, 24-Sep-2020.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = {⟨𝐴, 𝐵⟩}    ⇒   ⊢ (𝐴 = 𝐵 ↔ 𝐺 ∈ (V × V))
Theorem	ressnop0 6325	If 𝐴 is not in 𝐶, then the restriction of a singleton of ⟨𝐴, 𝐵⟩ to 𝐶 is null. (Contributed by Scott Fenton, 15-Apr-2011.)
⊢ (¬ 𝐴 ∈ 𝐶 → ({⟨𝐴, 𝐵⟩} ↾ 𝐶) = ∅)
Theorem	fpr 6326	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}:{𝐴, 𝐵}⟶{𝐶, 𝐷})
Theorem	fprg 6327	A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.)
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}:{𝐴, 𝐵}⟶{𝐶, 𝐷})
Theorem	ftpg 6328	A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶})
Theorem	ftp 6329	A function with a domain of three elements. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by Alexander van der Vekens, 23-Jan-2018.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    &   ⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐴 ≠ 𝐶    &   ⊢ 𝐵 ≠ 𝐶    ⇒   ⊢ {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩, ⟨𝐶, 𝑍⟩}:{𝐴, 𝐵, 𝐶}⟶{𝑋, 𝑌, 𝑍}
Theorem	fnressn 6330	A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {⟨𝐵, (𝐹‘𝐵)⟩})
Theorem	funressn 6331	A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (Fun 𝐹 → (𝐹 ↾ {𝐵}) ⊆ {⟨𝐵, (𝐹‘𝐵)⟩})
Theorem	fressnfv 6332	The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶))
Theorem	fvrnressn 6333	If the value of a function is in the range of the function restricted to the singleton containing the argument, then the value of the function is in the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
⊢ (𝑋 ∈ 𝑉 → ((𝐹‘𝑋) ∈ ran (𝐹 ↾ {𝑋}) → (𝐹‘𝑋) ∈ ran 𝐹))
Theorem	fvressn 6334	The value of a function restricted to the singleton containing the argument equals the value of the function for this argument. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
⊢ (𝑋 ∈ 𝑉 → ((𝐹 ↾ {𝑋})‘𝑋) = (𝐹‘𝑋))
Theorem	fvn0fvelrn 6335	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.)
⊢ ((𝐹‘𝑋) ≠ ∅ → (𝐹‘𝑋) ∈ ran 𝐹)
Theorem	fvconst 6336	The value of a constant function. (Contributed by NM, 30-May-1999.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵)
Theorem	fnsnb 6337	A function whose domain is a singleton can be represented as a singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Revised to add reverse implication. (Revised by NM, 29-Dec-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})
Theorem	fmptsn 6338*	Express a singleton function in maps-to notation. (Contributed by NM, 6-Jun-2006.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵))
Theorem	fmptsng 6339*	Express a singleton function in maps-to notation. Version of fmptsn 6338 allowing the mapping value to depend on the mapping variable (usual case). (Contributed by AV, 27-Feb-2019.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {⟨𝐴, 𝐶⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵))
Theorem	fmptsnd 6340*	Express a singleton function in maps-to notation. Deduction form of fmptsng 6339. (Contributed by AV, 4-Aug-2019.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐶⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵))
Theorem	fmptap 6341*	Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑅 ∪ {𝐴}) = 𝑆    &   ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐵)    ⇒   ⊢ ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶)
Theorem	fmptapd 6342*	Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → (𝑅 ∪ {𝐴}) = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶))
Theorem	fmptpr 6343*	Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸))
Theorem	fvresi 6344	The value of a restricted identity function. (Contributed by NM, 19-May-2004.)
⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)
Theorem	fninfp 6345*	Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∩ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝑥})
Theorem	fnelfp 6346	Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑋) = 𝑋))
Theorem	fndifnfp 6347*	Express the class of non-fixed points of a function. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∖ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ 𝑥})
Theorem	fnelnfp 6348	Property of a non-fixed point of a function. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋))
Theorem	fnnfpeq0 6349	A function is the identity iff it moves no points. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ (𝐹 Fn 𝐴 → (dom (𝐹 ∖ I ) = ∅ ↔ 𝐹 = ( I ↾ 𝐴)))
Theorem	fvunsn 6350	Remove an ordered pair not participating in a function value. (Contributed by NM, 1-Oct-2013.) (Revised by Mario Carneiro, 28-May-2014.)
⊢ (𝐵 ≠ 𝐷 → ((𝐴 ∪ {⟨𝐵, 𝐶⟩})‘𝐷) = (𝐴‘𝐷))
Theorem	fvsn 6351	The value of a singleton of an ordered pair is the second member. (Contributed by NM, 12-Aug-1994.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵
Theorem	fvsng 6352	The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵)
Theorem	fvsnun1 6353	The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 6354. (Contributed by NM, 23-Sep-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴})))    ⇒   ⊢ (𝐺‘𝐴) = 𝐵
Theorem	fvsnun2 6354	The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 6353. (Contributed by NM, 23-Sep-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴})))    ⇒   ⊢ (𝐷 ∈ (𝐶 ∖ {𝐴}) → (𝐺‘𝐷) = (𝐹‘𝐷))
Theorem	fnsnsplit 6355	Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐹 = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩}))
Theorem	fsnunf 6356	Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐹:𝑆⟶𝑇 ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):(𝑆 ∪ {𝑋})⟶𝑇)
Theorem	fsnunf2 6357	Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐹:(𝑆 ∖ {𝑋})⟶𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):𝑆⟶𝑇)
Theorem	fsnunfv 6358	Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
Theorem	fsnunres 6359	Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ 𝑆) = 𝐹)
Theorem	funresdfunsn 6360	Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself. (Contributed by AV, 2-Dec-2018.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ (V ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩}) = 𝐹)
Theorem	fvpr1 6361	The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐴) = 𝐶)
Theorem	fvpr2 6362	The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐵) = 𝐷)
Theorem	fvpr1g 6363	The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐴) = 𝐶)
Theorem	fvpr2g 6364	The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐵) = 𝐷)
Theorem	fvtp1 6365	The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷)
Theorem	fvtp2 6366	The second value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐸 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸)
Theorem	fvtp3 6367	The third value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹)
Theorem	fvtp1g 6368	The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷)
Theorem	fvtp2g 6369	The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸)
Theorem	fvtp3g 6370	The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹)
Theorem	tpres 6371	An unordered triple of ordered pairs restricted to all but one first components of the pairs is an unordered pair of ordered pairs. (Contributed by AV, 14-Mar-2020.)
⊢ (𝜑 → 𝑇 = {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐴)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐴)    ⇒   ⊢ (𝜑 → (𝑇 ↾ (V ∖ {𝐴})) = {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
Theorem	fvconst2g 6372	The value of a constant function. (Contributed by NM, 20-Aug-2005.)
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Theorem	fconst2g 6373	A constant function expressed as a Cartesian product. (Contributed by NM, 27-Nov-2007.)
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵})))
Theorem	fvconst2 6374	The value of a constant function. (Contributed by NM, 16-Apr-2005.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Theorem	fconst2 6375	A constant function expressed as a Cartesian product. (Contributed by NM, 20-Aug-1999.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵}))
Theorem	fconst5 6376	Two ways to express that a function is constant. (Contributed by NM, 27-Nov-2007.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅) → (𝐹 = (𝐴 × {𝐵}) ↔ ran 𝐹 = {𝐵}))
Theorem	fnprb 6377	A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by FL, 26-Jun-2011.) (Proof shortened by Scott Fenton, 12-Oct-2017.) Revised to eliminate unnecessary antecedent 𝐴 ≠ 𝐵. (Revised by NM, 29-Dec-2018.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
Theorem	fntpb 6378	A function whose domain has at most three elements can be represented as a set of at most three ordered pairs. (Contributed by AV, 26-Jan-2021.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩, ⟨𝐶, (𝐹‘𝐶)⟩})
Theorem	fnpr2g 6379	A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))
Theorem	fpr2g 6380	A function that maps a pair to a class is a pair of ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹:{𝐴, 𝐵}⟶𝐶 ↔ ((𝐹‘𝐴) ∈ 𝐶 ∧ (𝐹‘𝐵) ∈ 𝐶 ∧ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})))
Theorem	fconstfv 6381*	A constant function expressed in terms of its functionality, domain, and value. See also fconst2 6375. (Contributed by NM, 27-Aug-2004.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
Theorem	fconst3 6382	Two ways to express a constant function. (Contributed by NM, 15-Mar-2007.)
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ 𝐴 ⊆ (◡𝐹 “ {𝐵})))
Theorem	fconst4 6383	Two ways to express a constant function. (Contributed by NM, 8-Mar-2007.)
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ (◡𝐹 “ {𝐵}) = 𝐴))
Theorem	resfunexg 6384	The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. (Contributed by NM, 7-Apr-1995.) (Revised by Mario Carneiro, 22-Jun-2013.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V)
Theorem	resiexd 6385	The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ( I ↾ 𝐵) ∈ V)
Theorem	fnex 6386	If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg 6384. See fnexALT 7025 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V)
Theorem	funex 6387	If the domain of a function exists, so the function. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of fnex 6386. (Note: Any resemblance between F.U.N.E.X. and "Have You Any Eggs" is purely a coincidence originated by Swedish chefs.) (Contributed by NM, 11-Nov-1995.)
⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵) → 𝐹 ∈ V)
Theorem	opabex 6388*	Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → ∃*𝑦𝜑)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V
Theorem	mptexg 6389*	If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
Theorem	mptex 6390*	If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6389. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V
Theorem	mptexd 6391*	If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 6389. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
Theorem	mptrabex 6392*	If the domain of a function given by maps-to notation is a class abstraction based on a set, the function is a set. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↦ 𝐵) ∈ V
Theorem	mptrabexOLD 6393*	Obsolete version of mptrabex 6392 as of 26-Mar-2021. (Contributed by AV, 16-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↦ 𝐵) ∈ V
Theorem	fex 6394	If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)
Theorem	eufnfv 6395*	A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∃!𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝐵)
Theorem	funfvima 6396	A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003.)
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))
Theorem	funfvima2 6397	A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))
Theorem	resfvresima 6398	The value of the function value of a restriction for a function restricted to the image of the restricting subset. (Contributed by AV, 6-Mar-2021.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝑆 ⊆ dom 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐻 ↾ (𝐹 “ 𝑆))‘((𝐹 ↾ 𝑆)‘𝑋)) = (𝐻‘(𝐹‘𝑋)))
Theorem	funfvima3 6399	A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by NM, 23-Mar-2004.)
⊢ ((Fun 𝐹 ∧ 𝐹 ⊆ 𝐺) → (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) ∈ (𝐺 “ {𝐴})))
Theorem	fnfvima 6400	The function value of an operand in a set is contained in the image of that set, using the Fn abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))