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	f1fn 6801	A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹 Fn 𝐴)
Theorem	f1fun 6802	A one-to-one mapping is a function. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (𝐹:𝐴⟶1-1𝐵 → Fun 𝐹)
Theorem	f1funOLD 6803	Obsolete version of f1fun 6802 as of 10-Jun-2026. (Contributed by NM, 8-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐹:𝐴⟶1-1𝐵 → Fun 𝐹)
Theorem	f1rel 6804	A one-to-one onto mapping is a relation. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (𝐹:𝐴⟶1-1𝐵 → Rel 𝐹)
Theorem	f1relOLD 6805	Obsolete version of f1rel 6804 as of 10-Jun-2026. (Contributed by NM, 8-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐹:𝐴⟶1-1𝐵 → Rel 𝐹)
Theorem	f1dm 6806	The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Wolf Lammen, 29-May-2024.)
⊢ (𝐹:𝐴⟶1-1𝐵 → dom 𝐹 = 𝐴)
Theorem	f1ss 6807	A function that is one-to-one is also one-to-one on some superset of its codomain. (Contributed by Mario Carneiro, 12-Jan-2013.)
⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶1-1𝐶)
Theorem	f1ssr 6808	A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴⟶1-1𝐶)
Theorem	f1ssres 6809	A function that is one-to-one is also one-to-one on any subclass of its domain. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶1-1𝐵)
Theorem	f1resf1 6810	The restriction of an injective function is injective. (Contributed by AV, 28-Jun-2022.)
⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ (𝐹 ↾ 𝐶):𝐶⟶𝐷) → (𝐹 ↾ 𝐶):𝐶⟶1-1𝐷)
Theorem	f1cnvcnv 6811	Two ways to express that a set 𝐴 (not necessarily a function) is one-to-one. Each side is equivalent to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation "Un2 (A)" for one-to-one. We do not introduce a separate notation since we rarely use it. (Contributed by NM, 13-Aug-2004.)
⊢ (◡◡𝐴:dom 𝐴⟶1-1V ↔ (Fun ◡𝐴 ∧ Fun ◡◡𝐴))
Theorem	f1cof1 6812	Composition of two one-to-one functions. Generalization of f1co 6813. (Contributed by AV, 18-Sep-2024.)
⊢ ((𝐹:𝐶⟶1-1𝐷 ∧ 𝐺:𝐴⟶1-1𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐶)⟶1-1𝐷)
Theorem	f1co 6813	Composition of one-to-one functions when the codomain of the first matches the domain of the second. Exercise 30 of [TakeutiZaring] p. 25. (Contributed by NM, 28-May-1998.) (Proof shortened by AV, 20-Sep-2024.)
⊢ ((𝐹:𝐵⟶1-1𝐶 ∧ 𝐺:𝐴⟶1-1𝐵) → (𝐹 ∘ 𝐺):𝐴⟶1-1𝐶)
Theorem	foeq1 6814	Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶onto𝐵 ↔ 𝐺:𝐴⟶onto𝐵))
Theorem	foeq2 6815	Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶onto𝐶 ↔ 𝐹:𝐵⟶onto𝐶))
Theorem	foeq3 6816	Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶onto𝐴 ↔ 𝐹:𝐶⟶onto𝐵))
Theorem	nffo 6817	Bound-variable hypothesis builder for an onto function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴⟶onto𝐵
Theorem	fof 6818	An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴⟶onto𝐵 → 𝐹:𝐴⟶𝐵)
Theorem	fofun 6819	An onto mapping is a function. (Contributed by NM, 29-Mar-2008.)
⊢ (𝐹:𝐴⟶onto𝐵 → Fun 𝐹)
Theorem	fofn 6820	An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)
⊢ (𝐹:𝐴⟶onto𝐵 → 𝐹 Fn 𝐴)
Theorem	forn 6821	The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴⟶onto𝐵 → ran 𝐹 = 𝐵)
Theorem	dffo2 6822	Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.)
⊢ (𝐹:𝐴⟶onto𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
Theorem	foima 6823	The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002.)
⊢ (𝐹:𝐴⟶onto𝐵 → (𝐹 “ 𝐴) = 𝐵)
Theorem	dffn4 6824	A function maps onto its range. (Contributed by NM, 10-May-1998.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ontoran 𝐹)
Theorem	funforn 6825	A function maps its domain onto its range. (Contributed by NM, 23-Jul-2004.)
⊢ (Fun 𝐴 ↔ 𝐴:dom 𝐴⟶ontoran 𝐴)
Theorem	fodmrnu 6826	An onto function has unique domain and range. (Contributed by NM, 5-Nov-2006.)
⊢ ((𝐹:𝐴⟶onto𝐵 ∧ 𝐹:𝐶⟶onto𝐷) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	fimadmfo 6827	A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶onto(𝐹 “ 𝐴))
Theorem	fores 6828	Restriction of an onto function. (Contributed by NM, 4-Mar-1997.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴⟶onto(𝐹 “ 𝐴))
Theorem	fimadmfoALT 6829	Alternate proof of fimadmfo 6827, based on fores 6828. 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 6830	The preimage of the codomain of a surjection is its domain. (Contributed by AV, 29-Sep-2024.)
⊢ (𝐺:𝐴⟶onto𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
Theorem	focofo 6831	Composition of onto functions. Generalisation of foco 6832. (Contributed by AV, 29-Sep-2024.)
⊢ ((𝐹:𝐴⟶onto𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)⟶onto𝐵)
Theorem	foco 6832	Composition of onto functions. (Contributed by NM, 22-Mar-2006.) (Proof shortened by AV, 29-Sep-2024.)
⊢ ((𝐹:𝐵⟶onto𝐶 ∧ 𝐺:𝐴⟶onto𝐵) → (𝐹 ∘ 𝐺):𝐴⟶onto𝐶)
Theorem	foconst 6833	A nonzero constant function is onto. (Contributed by NM, 12-Jan-2007.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐹 ≠ ∅) → 𝐹:𝐴⟶onto{𝐵})
Theorem	f1oeq1 6834	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶1-1onto𝐵 ↔ 𝐺:𝐴⟶1-1onto𝐵))
Theorem	f1oeq2 6835	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶1-1onto𝐶 ↔ 𝐹:𝐵⟶1-1onto𝐶))
Theorem	f1oeq3 6836	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶1-1onto𝐴 ↔ 𝐹:𝐶⟶1-1onto𝐵))
Theorem	f1oeq23 6837	Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐹:𝐴⟶1-1onto𝐶 ↔ 𝐹:𝐵⟶1-1onto𝐷))
Theorem	f1eq123d 6838	Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶1-1𝐶 ↔ 𝐺:𝐵⟶1-1𝐷))
Theorem	foeq123d 6839	Equality deduction for onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶onto𝐶 ↔ 𝐺:𝐵⟶onto𝐷))
Theorem	f1oeq123d 6840	Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶1-1onto𝐶 ↔ 𝐺:𝐵⟶1-1onto𝐷))
Theorem	f1oeq1d 6841	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶1-1onto𝐵 ↔ 𝐺:𝐴⟶1-1onto𝐵))
Theorem	f1oeq2d 6842	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴⟶1-1onto𝐶 ↔ 𝐹:𝐵⟶1-1onto𝐶))
Theorem	f1oeq3d 6843	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐶⟶1-1onto𝐴 ↔ 𝐹:𝐶⟶1-1onto𝐵))
Theorem	nff1o 6844	Bound-variable hypothesis builder for a one-to-one onto function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴⟶1-1onto𝐵
Theorem	f1of1 6845	A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶1-1𝐵)
Theorem	f1of 6846	A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶𝐵)
Theorem	f1ofn 6847	A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹 Fn 𝐴)
Theorem	f1ofun 6848	A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 → Fun 𝐹)
Theorem	f1orel 6849	A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 → Rel 𝐹)
Theorem	f1odm 6850	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-1onto𝐵 → dom 𝐹 = 𝐴)
Theorem	f1odmOLD 6851	Obsolete version of f1odm 6850 as of 10-Jun-2026. (Contributed by NM, 8-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 → dom 𝐹 = 𝐴)
Theorem	dff1o2 6852	Alternate definition of one-to-one onto function. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
Theorem	dff1o3 6853	Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶onto𝐵 ∧ Fun ◡𝐹))
Theorem	f1ofo 6854	A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶onto𝐵)
Theorem	dff1o4 6855	Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
Theorem	dff1o5 6856	Alternate definition of one-to-one onto function. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 = 𝐵))
Theorem	f1orn 6857	A one-to-one function maps onto its range. (Contributed by NM, 13-Aug-2004.)
⊢ (𝐹:𝐴⟶1-1ontoran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
Theorem	f1f1orn 6858	A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.)
⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹:𝐴⟶1-1ontoran 𝐹)
Theorem	f1ocnv 6859	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-1onto𝐵 → ◡𝐹:𝐵⟶1-1onto𝐴)
Theorem	f1ocnvb 6860	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-1onto𝐵 ↔ ◡𝐹:𝐵⟶1-1onto𝐴))
Theorem	f1ores 6861	The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by NM, 25-Mar-1998.)
⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶1-1onto(𝐹 “ 𝐶))
Theorem	f1orescnv 6862	The converse of a one-to-one-onto restricted function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((Fun ◡𝐹 ∧ (𝐹 ↾ 𝑅):𝑅⟶1-1onto𝑃) → (◡𝐹 ↾ 𝑃):𝑃⟶1-1onto𝑅)
Theorem	f1imacnv 6863	Preimage of an image. (Contributed by NM, 30-Sep-2004.)
⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (◡𝐹 “ (𝐹 “ 𝐶)) = 𝐶)
Theorem	foimacnv 6864	A reverse version of f1imacnv 6863. (Contributed by Jeff Hankins, 16-Jul-2009.)
⊢ ((𝐹:𝐴⟶onto𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶)
Theorem	foun 6865	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 6866	The union of two one-to-one onto functions with disjoint domains and ranges. (Contributed by NM, 26-Mar-1998.)
⊢ (((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐺:𝐶⟶1-1onto𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)⟶1-1onto(𝐵 ∪ 𝐷))
Theorem	f1un 6867	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 6868	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-1onto(𝐶 ∖ 𝐷))
Theorem	resin 6869	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-1onto(𝐶 ∩ 𝐷))
Theorem	f1oco 6870	Composition of one-to-one onto functions. (Contributed by NM, 19-Mar-1998.)
⊢ ((𝐹:𝐵⟶1-1onto𝐶 ∧ 𝐺:𝐴⟶1-1onto𝐵) → (𝐹 ∘ 𝐺):𝐴⟶1-1onto𝐶)
Theorem	f1cnv 6871	The converse of an injective function is a bijection on its range. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴⟶1-1𝐵 → ◡𝐹:ran 𝐹⟶1-1onto𝐴)
Theorem	funcocnv2 6872	Precomposition with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by BJ, 25-Oct-2026.)
⊢ (Fun 𝐹 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹))
Theorem	funcocnv2OLD 6873	Obsolete version of funcocnv2 6872 as of 25-Oct-2026. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fun 𝐹 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹))
Theorem	fococnv2 6874	The composition of an onto function and its converse. (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ (𝐹:𝐴⟶onto𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
Theorem	f1ococnv2 6875	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-1onto𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
Theorem	f1cocnv2 6876	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴⟶1-1𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹))
Theorem	f1ococnv1 6877	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-1onto𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
Theorem	f1cocnv1 6878	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴⟶1-1𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
Theorem	funcoeqres 6879	Express a constraint on a composition as a constraint on the composand. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ ((Fun 𝐺 ∧ (𝐹 ∘ 𝐺) = 𝐻) → (𝐹 ↾ ran 𝐺) = (𝐻 ∘ ◡𝐺))
Theorem	f1ssf1 6880	A subset of an injective function is injective. (Contributed by AV, 20-Nov-2020.)
⊢ ((Fun 𝐹 ∧ Fun ◡𝐹 ∧ 𝐺 ⊆ 𝐹) → Fun ◡𝐺)
Theorem	f10 6881	The empty set maps one-to-one into any class. (Contributed by NM, 7-Apr-1998.)
⊢ ∅:∅⟶1-1𝐴
Theorem	f10d 6882	The empty set maps one-to-one into any class, deduction version. (Contributed by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐹 = ∅)    ⇒   ⊢ (𝜑 → 𝐹:dom 𝐹⟶1-1𝐴)
Theorem	f1o00 6883	One-to-one onto mapping of the empty set. (Contributed by NM, 15-Apr-1998.)
⊢ (𝐹:∅⟶1-1onto𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
Theorem	fo00 6884	Onto mapping of the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ (𝐹:∅⟶onto𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
Theorem	f1o0 6885	One-to-one onto mapping of the empty set. (Contributed by NM, 10-Sep-2004.)
⊢ ∅:∅⟶1-1onto∅
Theorem	f1oi 6886	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-1onto𝐴
Theorem	f1oiOLD 6887	Obsolete version of f1oi 6886 as of 10-Feb-2026. (Contributed by NM, 30-Apr-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ( I ↾ 𝐴):𝐴⟶1-1onto𝐴
Theorem	f1ovi 6888	The identity relation is a one-to-one onto function on the universe. (Contributed by NM, 16-May-2004.)
⊢ I :V⟶1-1ontoV
Theorem	f1osn 6889	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-1onto{𝐵}
Theorem	f1osng 6890	A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}⟶1-1onto{𝐵})
Theorem	f1sng 6891	A singleton of an ordered pair is a one-to-one function. (Contributed by AV, 17-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}⟶1-1𝑊)
Theorem	fsnd 6892	A singleton of an ordered pair is a function. (Contributed by AV, 17-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐵⟩}:{𝐴}⟶𝑊)
Theorem	f1oprswap 6893	A two-element swap is a bijection on a pair. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}:{𝐴, 𝐵}⟶1-1onto{𝐴, 𝐵})
Theorem	f1oprg 6894	An unordered pair of ordered pairs with different elements is a one-to-one onto function, analogous to f1oprswap 6893. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}:{𝐴, 𝐶}⟶1-1onto{𝐵, 𝐷}))
Theorem	tz6.12-2 6895*	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 6896*	Obsolete version of tz6.12-2 6895 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 6897*	The value of a function at a unique point. (Contributed by Scott Fenton, 6-Oct-2017.)
⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})
Theorem	brprcneu 6898*	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 6899 for a proof that uses ax-pow 5331 instead of ax-pr 5395. (Contributed by Scott Fenton, 7-Oct-2017.)
⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
Theorem	brprcneuALT 6899*	Alternate proof of brprcneu 6898 using ax-pow 5331 instead of ax-pr 5395. (Contributed by Scott Fenton, 7-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
Theorem	fvprc 6900	A function's value at a proper class is the empty set. See fvprcALT 6901 for a proof that uses ax-pow 5331 instead of ax-pr 5395. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5331. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.)
⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)