P. 72 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7101-7200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dffo5 7101*	Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦))
Theorem	exfo 7102*	A relation equivalent to the existence of an onto mapping. The right-hand 𝑓 is not necessarily a function. (Contributed by NM, 20-Mar-2007.)
⊢ (∃𝑓 𝑓:𝐴–onto→𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑦𝑓𝑥))
Theorem	dffo3f 7103*	An onto mapping expressed in terms of function values. As dffo3 7099 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))
Theorem	foelrn 7104*	Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥))
Theorem	foelrnf 7105*	Property of a surjective function. As foelrn 7104 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥))
Theorem	foco2 7106	If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵 ∧ (𝐹 ∘ 𝐺):𝐴–onto→𝐶) → 𝐹:𝐵–onto→𝐶)
Theorem	fmpt 7107*	Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	f1ompt 7108*	Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
Theorem	fmpti 7109*	Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    ⇒   ⊢ 𝐹:𝐴⟶𝐵
Theorem	fvmptelcdm 7110*	The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
Theorem	fmptd 7111*	Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fmpttd 7112*	Version of fmptd 7111 with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
Theorem	fmpt3d 7113*	Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fmptdf 7114*	A version of fmptd 7111 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fompt 7115*	Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (𝐹:𝐴–onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = 𝐶))
Theorem	ffnfv 7116*	A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	ffnfvf 7117	A function maps to a class to which all values belong. This version of ffnfv 7116 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	fnfvrnss 7118*	An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
Theorem	fcdmssb 7119*	A function is a function into a subset of its codomain if all of its values are elements of this subset. (Contributed by AV, 7-Feb-2021.)
⊢ ((𝑉 ⊆ 𝑊 ∧ ∀𝑘 ∈ 𝐴 (𝐹‘𝑘) ∈ 𝑉) → (𝐹:𝐴⟶𝑊 ↔ 𝐹:𝐴⟶𝑉))
Theorem	rnmptss 7120*	The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶)
Theorem	rnmptssd 7121*	The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶)
Theorem	fmpt2d 7122*	Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	ffvresb 7123*	A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (Fun 𝐹 → ((𝐹 ↾ 𝐴):𝐴⟶𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐵)))
Theorem	fssrescdmd 7124	Restriction of a function to a subclass of its domain as a function with domain and codomain. (Contributed by AV, 13-May-2025.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → (𝐹 “ 𝐶) ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐷)
Theorem	f1oresrab 7125*	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	f1ossf1o 7126*	Restricting a bijection, which is a mapping from a restricted class abstraction, to a subset is a bijection. (Contributed by AV, 7-Aug-2022.)
⊢ 𝑋 = {𝑤 ∈ 𝐴 ∣ (𝜓 ∧ 𝜒)}    &   ⊢ 𝑌 = {𝑤 ∈ 𝐴 ∣ 𝜓}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑌 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐺:𝑌–1-1-onto→𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 = 𝐵) → (𝜏 ↔ [𝑥 / 𝑤]𝜒))    ⇒   ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→{𝑦 ∈ 𝐶 ∣ 𝜏})
Theorem	fmptco 7127*	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 7128*	Version of fmptco 7127 where 𝜑 needn't be distinct from 𝑥. (Contributed by NM, 27-Dec-2014.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))
Theorem	fmptcos 7129*	Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ ⦋𝑅 / 𝑦⦌𝑆))
Theorem	cofmpt 7130*	Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
⊢ (𝜑 → 𝐹:𝐶⟶𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)))
Theorem	fcompt 7131*	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 7132	Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)}))
Theorem	fsn 7133	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 7134	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 7135	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 7136	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 7137	The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩})
Theorem	xpprsng 7138	The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} × {𝐶}) = {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐶⟩})
Theorem	xpsn 7139	The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by NM, 4-Nov-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩}
Theorem	f1o2sn 7140	A singleton consisting in a nested ordered pair is a one-to-one function from the cartesian product of two singletons onto a singleton (case where the two singletons are equal). (Contributed by AV, 15-Aug-2019.)
⊢ ((𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → {⟨⟨𝐸, 𝐸⟩, 𝑋⟩}:({𝐸} × {𝐸})–1-1-onto→{𝑋})
Theorem	residpr 7141	Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( I ↾ {𝐴, 𝐵}) = {⟨𝐴, 𝐴⟩, ⟨𝐵, 𝐵⟩})
Theorem	dfmpt 7142	Alternate definition for the maps-to notation df-mpt 5194 (although it requires that 𝐵 be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
Theorem	fnasrn 7143	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	idref 7144*	Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) (Revised by NM, 30-Mar-2016.)
⊢ (( I ↾ 𝐴) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥)
Theorem	funiun 7145*	A function is a union of singletons of ordered pairs indexed by its domain. (Contributed by AV, 18-Sep-2020.)
⊢ (Fun 𝐹 → 𝐹 = ∪ 𝑥 ∈ dom 𝐹{⟨𝑥, (𝐹‘𝑥)⟩})
Theorem	funopsn 7146*	If a function is an ordered pair then it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) (Proof shortened by AV, 15-Jul-2021.) (Proof shortened by Eric Schmidt, 9-May-2026.) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng 6589, as relsnopg 5792 is to relop 5838. (New usage is discouraged.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐹 = ⟨𝑋, 𝑌⟩) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {⟨𝑎, 𝑎⟩}))
Theorem	funopsnOLD 7147*	Obsolete version of funopsn 7146 as of 9-May-2026. (Contributed by AV, 20-Sep-2020.) (Proof shortened by AV, 15-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐹 = ⟨𝑋, 𝑌⟩) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {⟨𝑎, 𝑎⟩}))
Theorem	funop 7148*	An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng 6589, as relsnopg 5792 is to relop 5838. (New usage is discouraged.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    ⇒   ⊢ (Fun ⟨𝑋, 𝑌⟩ ↔ ∃𝑎(𝑋 = {𝑎} ∧ ⟨𝑋, 𝑌⟩ = {⟨𝑎, 𝑎⟩}))
Theorem	funopdmsn 7149	The domain of a function which is an ordered pair is a singleton. (Contributed by AV, 15-Nov-2021.) (Avoid depending on this detail.)
⊢ 𝐺 = ⟨𝑋, 𝑌⟩    &   ⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑌 ∈ 𝑊    ⇒   ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺) → 𝐴 = 𝐵)
Theorem	funsndifnop 7150	A singleton of an ordered pair is not an ordered pair if the components are different. (Contributed by AV, 23-Sep-2020.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = {⟨𝐴, 𝐵⟩}    ⇒   ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐺 ∈ (V × V))
Theorem	funsneqopb 7151	A singleton of an ordered pair is an ordered pair iff the components are equal. (Contributed by AV, 24-Sep-2020.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐺 = {⟨𝐴, 𝐵⟩}    ⇒   ⊢ (𝐴 = 𝐵 ↔ 𝐺 ∈ (V × V))
Theorem	ressnop0 7152	If 𝐴 is not in 𝐶, then the restriction of a singleton of ⟨𝐴, 𝐵⟩ to 𝐶 is null. (Contributed by Scott Fenton, 15-Apr-2011.)
⊢ (¬ 𝐴 ∈ 𝐶 → ({⟨𝐴, 𝐵⟩} ↾ 𝐶) = ∅)
Theorem	fpr 7153	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 7154	A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.)
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}:{𝐴, 𝐵}⟶{𝐶, 𝐷})
Theorem	ftpg 7155	A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶})
Theorem	ftp 7156	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 7157	A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {⟨𝐵, (𝐹‘𝐵)⟩})
Theorem	funressn 7158	A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (Fun 𝐹 → (𝐹 ↾ {𝐵}) ⊆ {⟨𝐵, (𝐹‘𝐵)⟩})
Theorem	fressnfv 7159	The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶))
Theorem	fvrnressn 7160	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 7161	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	fvconst 7162	The value of a constant function. (Contributed by NM, 30-May-1999.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵)
Theorem	fnsnr 7163	If a class belongs to a function on a singleton, then that class is the obvious ordered pair. Note that this theorem also holds when 𝐴 is a proper class, but its meaning is then different. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.)
⊢ (𝐹 Fn {𝐴} → (𝐵 ∈ 𝐹 → 𝐵 = ⟨𝐴, (𝐹‘𝐴)⟩))
Theorem	fnsnbg 7164	A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023.) Relax condition for being in the universal class. (Revised by Zhi Wang, 21-Oct-2025.)
⊢ (𝐴 ∈ 𝑉 → (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩}))
Theorem	fnsnb 7165	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.) (Proof shortened by Zhi Wang, 21-Oct-2025.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})
Theorem	fnsnbOLD 7166	Obsolete version of fnsnb 7165 as of 21-Oct-2025. 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.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})
Theorem	fmptsn 7167*	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 7168*	Express a singleton function in maps-to notation. Version of fmptsn 7167 allowing the value 𝐵 to depend on the variable 𝑥. (Contributed by AV, 27-Feb-2019.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {⟨𝐴, 𝐶⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵))
Theorem	fmptsnd 7169*	Express a singleton function in maps-to notation. Deduction form of fmptsng 7168. (Contributed by AV, 4-Aug-2019.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐶⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵))
Theorem	fmptap 7170*	Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑅 ∪ {𝐴}) = 𝑆    &   ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐵)    ⇒   ⊢ ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶)
Theorem	fmptapd 7171*	Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.) (Revised by AV, 10-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑅 ∪ {𝐴}) = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶))
Theorem	fmptpr 7172*	Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸))
Theorem	fvresi 7173	The value of a restricted identity function. (Contributed by NM, 19-May-2004.)
⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)
Theorem	fninfp 7174*	Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∩ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝑥})
Theorem	fnelfp 7175	Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑋) = 𝑋))
Theorem	fndifnfp 7176*	Express the class of non-fixed points of a function. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∖ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ 𝑥})
Theorem	fnelnfp 7177	Property of a non-fixed point of a function. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋))
Theorem	fnnfpeq0 7178	A function is the identity iff it moves no points. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ (𝐹 Fn 𝐴 → (dom (𝐹 ∖ I ) = ∅ ↔ 𝐹 = ( I ↾ 𝐴)))
Theorem	fvunsn 7179	Remove an ordered pair not participating in a function value. (Contributed by NM, 1-Oct-2013.) (Revised by Mario Carneiro, 28-May-2014.)
⊢ (𝐵 ≠ 𝐷 → ((𝐴 ∪ {⟨𝐵, 𝐶⟩})‘𝐷) = (𝐴‘𝐷))
Theorem	fvsng 7180	The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012.) (Proof shortened by BJ, 25-Feb-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵)
Theorem	fvsn 7181	The value of a singleton of an ordered pair is the second member. (Contributed by NM, 12-Aug-1994.) (Proof shortened by BJ, 25-Feb-2023.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵
Theorem	fvsnun1 7182	The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7183. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴})))    ⇒   ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵)
Theorem	fvsnun2 7183	The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 7182. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴})))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐶 ∖ {𝐴}))    ⇒   ⊢ (𝜑 → (𝐺‘𝐷) = (𝐹‘𝐷))
Theorem	fnsnsplit 7184	Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐹 = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩}))
Theorem	fsnunf 7185	Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐹:𝑆⟶𝑇 ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):(𝑆 ∪ {𝑋})⟶𝑇)
Theorem	fsnunf2 7186	Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐹:(𝑆 ∖ {𝑋})⟶𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):𝑆⟶𝑇)
Theorem	fsnunfv 7187	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 7188	Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ 𝑆) = 𝐹)
Theorem	funresdfunsn 7189	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	fvpr1g 7190	The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐴) = 𝐶)
Theorem	fvpr2g 7191	The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Proof shortened by BJ, 26-Sep-2024.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐵) = 𝐷)
Theorem	fvpr1 7192	The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by BJ, 26-Sep-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐴) = 𝐶)
Theorem	fvpr2 7193	The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by BJ, 26-Sep-2024.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐵) = 𝐷)
Theorem	fprb 7194*	A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}))
Theorem	fvtp1 7195	The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷)
Theorem	fvtp2 7196	The second value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐸 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸)
Theorem	fvtp3 7197	The third value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹)
Theorem	fvtp1g 7198	The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷)
Theorem	fvtp2g 7199	The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸)
Theorem	fvtp3g 7200	The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹)