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	fmptco 7101*	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 7102*	Version of fmptco 7101 where 𝜑 needn't be distinct from 𝑥. (Contributed by NM, 27-Dec-2014.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))
Theorem	fmptcos 7103*	Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ ⦋𝑅 / 𝑦⦌𝑆))
Theorem	cofmpt 7104*	Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
⊢ (𝜑 → 𝐹:𝐶⟶𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)))
Theorem	fcompt 7105*	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 7106	Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)}))
Theorem	fsn 7107	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 7108	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 7109	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 7110	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 7111	The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩})
Theorem	xpprsng 7112	The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} × {𝐶}) = {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐶⟩})
Theorem	xpsn 7113	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 7114	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 7115	Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( I ↾ {𝐴, 𝐵}) = {⟨𝐴, 𝐴⟩, ⟨𝐵, 𝐵⟩})
Theorem	dfmpt 7116	Alternate definition for the maps-to notation df-mpt 5189 (although it requires that 𝐵 be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}
Theorem	fnasrn 7117	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 7118*	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 7119*	A function is a union of singletons of ordered pairs indexed by its domain. (Contributed by AV, 18-Sep-2020.)
⊢ (Fun 𝐹 → 𝐹 = ∪ 𝑥 ∈ dom 𝐹{⟨𝑥, (𝐹‘𝑥)⟩})
Theorem	funopsn 7120*	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.) 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 6567, as relsnopg 5766 is to relop 5814. (New usage is discouraged.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐹 = ⟨𝑋, 𝑌⟩) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {⟨𝑎, 𝑎⟩}))
Theorem	funop 7121*	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 6567, as relsnopg 5766 is to relop 5814. (New usage is discouraged.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    ⇒   ⊢ (Fun ⟨𝑋, 𝑌⟩ ↔ ∃𝑎(𝑋 = {𝑎} ∧ ⟨𝑋, 𝑌⟩ = {⟨𝑎, 𝑎⟩}))
Theorem	funopdmsn 7122	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 7123	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 7124	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 7125	If 𝐴 is not in 𝐶, then the restriction of a singleton of ⟨𝐴, 𝐵⟩ to 𝐶 is null. (Contributed by Scott Fenton, 15-Apr-2011.)
⊢ (¬ 𝐴 ∈ 𝐶 → ({⟨𝐴, 𝐵⟩} ↾ 𝐶) = ∅)
Theorem	fpr 7126	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 7127	A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.)
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}:{𝐴, 𝐵}⟶{𝐶, 𝐷})
Theorem	ftpg 7128	A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶})
Theorem	ftp 7129	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 7130	A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {⟨𝐵, (𝐹‘𝐵)⟩})
Theorem	funressn 7131	A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (Fun 𝐹 → (𝐹 ↾ {𝐵}) ⊆ {⟨𝐵, (𝐹‘𝐵)⟩})
Theorem	fressnfv 7132	The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶))
Theorem	fvrnressn 7133	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 7134	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	fvn0fvelrnOLD 7135	Obsolete version of fvn0fvelrn 6889 as of 13-Jan-2025. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐹‘𝑋) ≠ ∅ → (𝐹‘𝑋) ∈ ran 𝐹)
Theorem	fvconst 7136	The value of a constant function. (Contributed by NM, 30-May-1999.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵)
Theorem	fnsnr 7137	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 7138	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 7139	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 7140	Obsolete version of fnsnb 7139 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 7141*	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 7142*	Express a singleton function in maps-to notation. Version of fmptsn 7141 allowing the value 𝐵 to depend on the variable 𝑥. (Contributed by AV, 27-Feb-2019.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {⟨𝐴, 𝐶⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵))
Theorem	fmptsnd 7143*	Express a singleton function in maps-to notation. Deduction form of fmptsng 7142. (Contributed by AV, 4-Aug-2019.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐶⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵))
Theorem	fmptap 7144*	Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑅 ∪ {𝐴}) = 𝑆    &   ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐵)    ⇒   ⊢ ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶)
Theorem	fmptapd 7145*	Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.) (Revised by AV, 10-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑅 ∪ {𝐴}) = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶))
Theorem	fmptpr 7146*	Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸))
Theorem	fvresi 7147	The value of a restricted identity function. (Contributed by NM, 19-May-2004.)
⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)
Theorem	fninfp 7148*	Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∩ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝑥})
Theorem	fnelfp 7149	Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑋) = 𝑋))
Theorem	fndifnfp 7150*	Express the class of non-fixed points of a function. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∖ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ 𝑥})
Theorem	fnelnfp 7151	Property of a non-fixed point of a function. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋))
Theorem	fnnfpeq0 7152	A function is the identity iff it moves no points. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ (𝐹 Fn 𝐴 → (dom (𝐹 ∖ I ) = ∅ ↔ 𝐹 = ( I ↾ 𝐴)))
Theorem	fvunsn 7153	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 7154	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 7155	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 7156	The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7157. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴})))    ⇒   ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵)
Theorem	fvsnun2 7157	The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 7156. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴})))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐶 ∖ {𝐴}))    ⇒   ⊢ (𝜑 → (𝐺‘𝐷) = (𝐹‘𝐷))
Theorem	fnsnsplit 7158	Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐹 = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩}))
Theorem	fsnunf 7159	Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐹:𝑆⟶𝑇 ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):(𝑆 ∪ {𝑋})⟶𝑇)
Theorem	fsnunf2 7160	Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐹:(𝑆 ∖ {𝑋})⟶𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):𝑆⟶𝑇)
Theorem	fsnunfv 7161	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 7162	Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ 𝑆) = 𝐹)
Theorem	funresdfunsn 7163	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 7164	The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐴) = 𝐶)
Theorem	fvpr2g 7165	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 7166	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 7167	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 7168*	A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}))
Theorem	fvtp1 7169	The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷)
Theorem	fvtp2 7170	The second value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐸 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸)
Theorem	fvtp3 7171	The third value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹)
Theorem	fvtp1g 7172	The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷)
Theorem	fvtp2g 7173	The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸)
Theorem	fvtp3g 7174	The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹)
Theorem	tpres 7175	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 7176	The value of a constant function. (Contributed by NM, 20-Aug-2005.)
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Theorem	fconst2g 7177	A constant function expressed as a Cartesian product. (Contributed by NM, 27-Nov-2007.)
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵})))
Theorem	fvconst2 7178	The value of a constant function. (Contributed by NM, 16-Apr-2005.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Theorem	fconst2 7179	A constant function expressed as a Cartesian product. (Contributed by NM, 20-Aug-1999.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵}))
Theorem	fconst5 7180	Two ways to express that a function is constant. (Contributed by NM, 27-Nov-2007.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅) → (𝐹 = (𝐴 × {𝐵}) ↔ ran 𝐹 = {𝐵}))
Theorem	rnmptc 7181*	Range of a constant function in maps-to notation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Remove extra hypothesis. (Revised by SN, 17-Apr-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ran 𝐹 = {𝐵})
Theorem	fnprb 7182	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.) Eliminate unnecessary antecedent 𝐴 ≠ 𝐵. (Revised by NM, 29-Dec-2018.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})
Theorem	fntpb 7183	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 7184	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 7185	A function that maps a pair to a class is a pair of ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹:{𝐴, 𝐵}⟶𝐶 ↔ ((𝐹‘𝐴) ∈ 𝐶 ∧ (𝐹‘𝐵) ∈ 𝐶 ∧ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})))
Theorem	fconstfv 7186*	A constant function expressed in terms of its functionality, domain, and value. See also fconst2 7179. (Contributed by NM, 27-Aug-2004.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
Theorem	fconst3 7187	Two ways to express a constant function. (Contributed by NM, 15-Mar-2007.)
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ 𝐴 ⊆ (◡𝐹 “ {𝐵})))
Theorem	fconst4 7188	Two ways to express a constant function. (Contributed by NM, 8-Mar-2007.)
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ (◡𝐹 “ {𝐵}) = 𝐴))
Theorem	resfunexg 7189	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 7190	The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ( I ↾ 𝐵) ∈ V)
Theorem	fnex 7191	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 7189. See fnexALT 7929 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V)
Theorem	fnexd 7192	If the domain of a function is a set, the function is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ∈ V)
Theorem	funex 7193	If the domain of a function exists, so does 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 7191. (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 7194*	Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → ∃*𝑦𝜑)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V
Theorem	mptexg 7195*	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	mptexgf 7196	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.) (Revised by Thierry Arnoux, 17-May-2020.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
Theorem	mptex 7197*	If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7195. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V
Theorem	mptexd 7198*	If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 7195. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
Theorem	mptrabex 7199*	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	fex 7200	If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)