P. 69 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6801-6900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fofn 6801	An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)
Theorem	forn 6802	The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
Theorem	dffo2 6803	Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
Theorem	foima 6804	The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002.)
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)
Theorem	dffn4 6805	A function maps onto its range. (Contributed by NM, 10-May-1998.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)
Theorem	funforn 6806	A function maps its domain onto its range. (Contributed by NM, 23-Jul-2004.)
⊢ (Fun 𝐴 ↔ 𝐴:dom 𝐴–onto→ran 𝐴)
Theorem	fodmrnu 6807	An onto function has unique domain and range. (Contributed by NM, 5-Nov-2006.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐹:𝐶–onto→𝐷) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	fimadmfo 6808	A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→(𝐹 “ 𝐴))
Theorem	fores 6809	Restriction of an onto function. (Contributed by NM, 4-Mar-1997.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴))
Theorem	fimadmfoALT 6810	Alternate proof of fimadmfo 6808, based on fores 6809. A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→(𝐹 “ 𝐴))
Theorem	focnvimacdmdm 6811	The preimage of the codomain of a surjection is its domain. (Contributed by AV, 29-Sep-2024.)
⊢ (𝐺:𝐴–onto→𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
Theorem	focofo 6812	Composition of onto functions. Generalisation of foco 6813. (Contributed by AV, 29-Sep-2024.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)–onto→𝐵)
Theorem	foco 6813	Composition of onto functions. (Contributed by NM, 22-Mar-2006.) (Proof shortened by AV, 29-Sep-2024.)
⊢ ((𝐹:𝐵–onto→𝐶 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–onto→𝐶)
Theorem	foconst 6814	A nonzero constant function is onto. (Contributed by NM, 12-Jan-2007.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐹 ≠ ∅) → 𝐹:𝐴–onto→{𝐵})
Theorem	f1oeq1 6815	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
Theorem	f1oeq2 6816	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	f1oeq3 6817	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
Theorem	f1oeq23 6818	Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷))
Theorem	f1eq123d 6819	Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷))
Theorem	foeq123d 6820	Equality deduction for onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–onto→𝐶 ↔ 𝐺:𝐵–onto→𝐷))
Theorem	f1oeq123d 6821	Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
Theorem	f1oeq1d 6822	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
Theorem	f1oeq2d 6823	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	f1oeq3d 6824	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
Theorem	nff1o 6825	Bound-variable hypothesis builder for a one-to-one onto function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴–1-1-onto→𝐵
Theorem	f1of1 6826	A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
Theorem	f1of 6827	A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
Theorem	f1ofn 6828	A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
Theorem	f1ofun 6829	A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹)
Theorem	f1orel 6830	A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
Theorem	f1odm 6831	The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)
Theorem	f1odmOLD 6832	Obsolete version of f1odm 6831 as of 10-Jun-2026. (Contributed by NM, 8-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)
Theorem	dff1o2 6833	Alternate definition of one-to-one onto function. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
Theorem	dff1o3 6834	Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
Theorem	f1ofo 6835	A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
Theorem	dff1o4 6836	Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
Theorem	dff1o5 6837	Alternate definition of one-to-one onto function. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))
Theorem	f1orn 6838	A one-to-one function maps onto its range. (Contributed by NM, 13-Aug-2004.)
⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
Theorem	f1f1orn 6839	A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.)
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)
Theorem	f1ocnv 6840	The converse of a one-to-one onto function is also one-to-one onto. (Contributed by NM, 11-Feb-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
Theorem	f1ocnvb 6841	A relation is a one-to-one onto function iff its converse is a one-to-one onto function with domain and codomain/range interchanged. (Contributed by NM, 8-Dec-2003.)
⊢ (Rel 𝐹 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹:𝐵–1-1-onto→𝐴))
Theorem	f1ores 6842	The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by NM, 25-Mar-1998.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶))
Theorem	f1orescnv 6843	The converse of a one-to-one-onto restricted function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((Fun ◡𝐹 ∧ (𝐹 ↾ 𝑅):𝑅–1-1-onto→𝑃) → (◡𝐹 ↾ 𝑃):𝑃–1-1-onto→𝑅)
Theorem	f1imacnv 6844	Preimage of an image. (Contributed by NM, 30-Sep-2004.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (◡𝐹 “ (𝐹 “ 𝐶)) = 𝐶)
Theorem	foimacnv 6845	A reverse version of f1imacnv 6844. (Contributed by Jeff Hankins, 16-Jul-2009.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶)
Theorem	foun 6846	The union of two onto functions with disjoint domains is an onto function. (Contributed by Mario Carneiro, 22-Jun-2016.)
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐶–onto→𝐷) ∧ (𝐴 ∩ 𝐶) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–onto→(𝐵 ∪ 𝐷))
Theorem	f1oun 6847	The union of two one-to-one onto functions with disjoint domains and ranges. (Contributed by NM, 26-Mar-1998.)
⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1-onto→(𝐵 ∪ 𝐷))
Theorem	f1un 6848	The union of two one-to-one functions with disjoint domains and codomains. (Contributed by BTernaryTau, 3-Dec-2024.)
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1→(𝐵 ∪ 𝐷))
Theorem	resdif 6849	The restriction of a one-to-one onto function to a difference maps onto the difference of the images. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ ((Fun ◡𝐹 ∧ (𝐹 ↾ 𝐴):𝐴–onto→𝐶 ∧ (𝐹 ↾ 𝐵):𝐵–onto→𝐷) → (𝐹 ↾ (𝐴 ∖ 𝐵)):(𝐴 ∖ 𝐵)–1-1-onto→(𝐶 ∖ 𝐷))
Theorem	resin 6850	The restriction of a one-to-one onto function to an intersection maps onto the intersection of the images. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ ((Fun ◡𝐹 ∧ (𝐹 ↾ 𝐴):𝐴–onto→𝐶 ∧ (𝐹 ↾ 𝐵):𝐵–onto→𝐷) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)–1-1-onto→(𝐶 ∩ 𝐷))
Theorem	f1oco 6851	Composition of one-to-one onto functions. (Contributed by NM, 19-Mar-1998.)
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝐺:𝐴–1-1-onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1-onto→𝐶)
Theorem	f1cnv 6852	The converse of an injective function is bijective. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴–1-1→𝐵 → ◡𝐹:ran 𝐹–1-1-onto→𝐴)
Theorem	funcocnv2 6853	Composition with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹))
Theorem	fococnv2 6854	The composition of an onto function and its converse. (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
Theorem	f1ococnv2 6855	The composition of a one-to-one onto function and its converse equals the identity relation restricted to the function's range. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Stefan O'Rear, 12-Feb-2015.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
Theorem	f1cocnv2 6856	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹))
Theorem	f1ococnv1 6857	The composition of a one-to-one onto function's converse and itself equals the identity relation restricted to the function's domain. (Contributed by NM, 13-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
Theorem	f1cocnv1 6858	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴–1-1→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
Theorem	funcoeqres 6859	Express a constraint on a composition as a constraint on the composand. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ ((Fun 𝐺 ∧ (𝐹 ∘ 𝐺) = 𝐻) → (𝐹 ↾ ran 𝐺) = (𝐻 ∘ ◡𝐺))
Theorem	f1ssf1 6860	A subset of an injective function is injective. (Contributed by AV, 20-Nov-2020.)
⊢ ((Fun 𝐹 ∧ Fun ◡𝐹 ∧ 𝐺 ⊆ 𝐹) → Fun ◡𝐺)
Theorem	f10 6861	The empty set maps one-to-one into any class. (Contributed by NM, 7-Apr-1998.)
⊢ ∅:∅–1-1→𝐴
Theorem	f10d 6862	The empty set maps one-to-one into any class, deduction version. (Contributed by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐹 = ∅)    ⇒   ⊢ (𝜑 → 𝐹:dom 𝐹–1-1→𝐴)
Theorem	f1o00 6863	One-to-one onto mapping of the empty set. (Contributed by NM, 15-Apr-1998.)
⊢ (𝐹:∅–1-1-onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
Theorem	fo00 6864	Onto mapping of the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ (𝐹:∅–onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
Theorem	f1o0 6865	One-to-one onto mapping of the empty set. (Contributed by NM, 10-Sep-2004.)
⊢ ∅:∅–1-1-onto→∅
Theorem	f1oi 6866	A restriction of the identity relation is a one-to-one onto function. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) Avoid ax-12 2216. (Revised by TM, 10-Feb-2026.)
⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
Theorem	f1oiOLD 6867	Obsolete version of f1oi 6866 as of 10-Feb-2026. (Contributed by NM, 30-Apr-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
Theorem	f1ovi 6868	The identity relation is a one-to-one onto function on the universe. (Contributed by NM, 16-May-2004.)
⊢ I :V–1-1-onto→V
Theorem	f1osn 6869	A singleton of an ordered pair is one-to-one onto function. (Contributed by NM, 18-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}
Theorem	f1osng 6870	A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})
Theorem	f1sng 6871	A singleton of an ordered pair is a one-to-one function. (Contributed by AV, 17-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1→𝑊)
Theorem	fsnd 6872	A singleton of an ordered pair is a function. (Contributed by AV, 17-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐵⟩}:{𝐴}⟶𝑊)
Theorem	f1oprswap 6873	A two-element swap is a bijection on a pair. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵})
Theorem	f1oprg 6874	An unordered pair of ordered pairs with different elements is a one-to-one onto function, analogous to f1oprswap 6873. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}:{𝐴, 𝐶}–1-1-onto→{𝐵, 𝐷}))
Theorem	tz6.12-2 6875*	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 2179, ax-11 2195, ax-12 2216. (Revised by TM, 25-Jan-2026.)
⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
Theorem	tz6.12-2OLD 6876*	Obsolete version of tz6.12-2 6875 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 6877*	The value of a function at a unique point. (Contributed by Scott Fenton, 6-Oct-2017.)
⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})
Theorem	brprcneu 6878*	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 6879 for a proof that uses ax-pow 5341 instead of ax-pr 5409. (Contributed by Scott Fenton, 7-Oct-2017.)
⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
Theorem	brprcneuALT 6879*	Alternate proof of brprcneu 6878 using ax-pow 5341 instead of ax-pr 5409. (Contributed by Scott Fenton, 7-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
Theorem	fvprc 6880	A function's value at a proper class is the empty set. See fvprcALT 6881 for a proof that uses ax-pow 5341 instead of ax-pr 5409. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5341. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.)
⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
Theorem	fvprcALT 6881	Alternate proof of fvprc 6880 using ax-pow 5341 instead of ax-pr 5409. (Contributed by NM, 20-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
Theorem	rnfvprc 6882	The range of a function value at a proper class is empty. (Contributed by AV, 20-Aug-2022.)
⊢ 𝑌 = (𝐹‘𝑋)    ⇒   ⊢ (¬ 𝑋 ∈ V → ran 𝑌 = ∅)
Theorem	fv2 6883*	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 6884*	A definition of function value in terms of iota. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐹‘𝐴) = (℩𝑥𝑥 ∈ (𝐹 “ {𝐴}))
Theorem	dffv4 6885*	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 6099), this definition apparently does not appear in the literature. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹‘𝐴) = ∪ {𝑥 ∣ (𝐹 “ {𝐴}) = {𝑥}}
Theorem	elfv 6886*	Membership in a function value. (Contributed by NM, 30-Apr-2004.)
⊢ (𝐴 ∈ (𝐹‘𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)))
Theorem	fveq1 6887	Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
Theorem	fveq2 6888	Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
Theorem	fveq1i 6889	Equality inference for function value. (Contributed by NM, 2-Sep-2003.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)
Theorem	fveq1d 6890	Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))
Theorem	fveq2i 6891	Equality inference for function value. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)
Theorem	fveq2d 6892	Equality deduction for function value. (Contributed by NM, 29-May-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))
Theorem	2fveq3 6893	Equality theorem for nested function values. (Contributed by AV, 14-Aug-2022.)
⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵)))
Theorem	fveq12i 6894	Equality deduction for function value. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐹 = 𝐺    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹‘𝐴) = (𝐺‘𝐵)
Theorem	fveq12d 6895	Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))
Theorem	fveqeq2d 6896	Equality deduction for function value. (Contributed by BJ, 30-Aug-2022.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))
Theorem	fveqeq2 6897	Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.)
⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))
Theorem	nffv 6898	Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹‘𝐴)
Theorem	nffvmpt1 6899*	Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶)
Theorem	nffvd 6900	Deduction version of bound-variable hypothesis builder nffv 6898. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐹‘𝐴))