P. 68 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6701-6800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fresaunres1 6701	From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐴) = 𝐹)
Theorem	fcoi1 6702	Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
Theorem	fcoi2 6703	Composition of restricted identity and a mapping. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
Theorem	feu 6704*	There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ∃!𝑦 ∈ 𝐵 ⟨𝐶, 𝑦⟩ ∈ 𝐹)
Theorem	fcnvres 6705	The converse of a restriction of a function. (Contributed by NM, 26-Mar-1998.)
⊢ (𝐹:𝐴⟶𝐵 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ 𝐵))
Theorem	fimacnvdisj 6706	The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (◡𝐹 “ 𝐶) = ∅)
Theorem	fint 6707*	Function into an intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ 𝐵 ≠ ∅    ⇒   ⊢ (𝐹:𝐴⟶∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐹:𝐴⟶𝑥)
Theorem	fin 6708	Mapping into an intersection. (Contributed by NM, 14-Sep-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶(𝐵 ∩ 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴⟶𝐶))
Theorem	f0 6709	The empty function. (Contributed by NM, 14-Aug-1999.)
⊢ ∅:∅⟶𝐴
Theorem	f00 6710	A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003.)
⊢ (𝐹:𝐴⟶∅ ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
Theorem	f0bi 6711	A function with empty domain is empty. (Contributed by Alexander van der Vekens, 30-Jun-2018.)
⊢ (𝐹:∅⟶𝑋 ↔ 𝐹 = ∅)
Theorem	f0dom0 6712	A function is empty iff it has an empty domain. (Contributed by AV, 10-Feb-2019.)
⊢ (𝐹:𝑋⟶𝑌 → (𝑋 = ∅ ↔ 𝐹 = ∅))
Theorem	f0rn0 6713*	If there is no element in the range of a function, its domain must be empty. (Contributed by Alexander van der Vekens, 12-Jul-2018.)
⊢ ((𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸) → 𝑋 = ∅)
Theorem	fconst 6714	A Cartesian product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵}
Theorem	fconstg 6715	A Cartesian product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
Theorem	fnconstg 6716	A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴)
Theorem	fconst6g 6717	Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶)
Theorem	fconst6 6718	A constant function as a mapping. (Contributed by Jeff Madsen, 30-Nov-2009.) (Revised by Mario Carneiro, 22-Apr-2015.)
⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ (𝐴 × {𝐵}):𝐴⟶𝐶
Theorem	f1eq1 6719	Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
Theorem	f1eq2 6720	Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
Theorem	f1eq3 6721	Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
Theorem	nff1 6722	Bound-variable hypothesis builder for a one-to-one function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴–1-1→𝐵
Theorem	dff12 6723*	Alternate definition of a one-to-one function. (Contributed by NM, 31-Dec-1996.)
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦∃*𝑥 𝑥𝐹𝑦))
Theorem	f1f 6724	A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
Theorem	f1fn 6725	A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
Theorem	f1fun 6726	A one-to-one mapping is a function. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)
Theorem	f1rel 6727	A one-to-one onto mapping is a relation. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴–1-1→𝐵 → Rel 𝐹)
Theorem	f1dm 6728	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 6729	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 6730	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 6731	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 6732	The restriction of an injective function is injective. (Contributed by AV, 28-Jun-2022.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ (𝐹 ↾ 𝐶):𝐶⟶𝐷) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐷)
Theorem	f1cnvcnv 6733	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-1→V ↔ (Fun ◡𝐴 ∧ Fun ◡◡𝐴))
Theorem	f1cof1 6734	Composition of two one-to-one functions. Generalization of f1co 6735. (Contributed by AV, 18-Sep-2024.)
⊢ ((𝐹:𝐶–1-1→𝐷 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐶)–1-1→𝐷)
Theorem	f1co 6735	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 6736	Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
Theorem	foeq2 6737	Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
Theorem	foeq3 6738	Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
Theorem	nffo 6739	Bound-variable hypothesis builder for an onto function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴–onto→𝐵
Theorem	fof 6740	An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
Theorem	fofun 6741	An onto mapping is a function. (Contributed by NM, 29-Mar-2008.)
⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹)
Theorem	fofn 6742	An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)
Theorem	forn 6743	The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
Theorem	dffo2 6744	Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
Theorem	foima 6745	The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002.)
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)
Theorem	dffn4 6746	A function maps onto its range. (Contributed by NM, 10-May-1998.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)
Theorem	funforn 6747	A function maps its domain onto its range. (Contributed by NM, 23-Jul-2004.)
⊢ (Fun 𝐴 ↔ 𝐴:dom 𝐴–onto→ran 𝐴)
Theorem	fodmrnu 6748	An onto function has unique domain and range. (Contributed by NM, 5-Nov-2006.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐹:𝐶–onto→𝐷) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	fimadmfo 6749	A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→(𝐹 “ 𝐴))
Theorem	fores 6750	Restriction of an onto function. (Contributed by NM, 4-Mar-1997.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴))
Theorem	fimadmfoALT 6751	Alternate proof of fimadmfo 6749, based on fores 6750. 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 6752	The preimage of the codomain of a surjection is its domain. (Contributed by AV, 29-Sep-2024.)
⊢ (𝐺:𝐴–onto→𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
Theorem	focofo 6753	Composition of onto functions. Generalisation of foco 6754. (Contributed by AV, 29-Sep-2024.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)–onto→𝐵)
Theorem	foco 6754	Composition of onto functions. (Contributed by NM, 22-Mar-2006.) (Proof shortened by AV, 29-Sep-2024.)
⊢ ((𝐹:𝐵–onto→𝐶 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–onto→𝐶)
Theorem	foconst 6755	A nonzero constant function is onto. (Contributed by NM, 12-Jan-2007.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐹 ≠ ∅) → 𝐹:𝐴–onto→{𝐵})
Theorem	f1oeq1 6756	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
Theorem	f1oeq2 6757	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	f1oeq3 6758	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
Theorem	f1oeq23 6759	Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷))
Theorem	f1eq123d 6760	Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷))
Theorem	foeq123d 6761	Equality deduction for onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–onto→𝐶 ↔ 𝐺:𝐵–onto→𝐷))
Theorem	f1oeq123d 6762	Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
Theorem	f1oeq1d 6763	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
Theorem	f1oeq2d 6764	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	f1oeq3d 6765	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
Theorem	nff1o 6766	Bound-variable hypothesis builder for a one-to-one onto function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴–1-1-onto→𝐵
Theorem	f1of1 6767	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 6768	A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
Theorem	f1ofn 6769	A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
Theorem	f1ofun 6770	A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹)
Theorem	f1orel 6771	A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
Theorem	f1odm 6772	The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)
Theorem	dff1o2 6773	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 6774	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 6775	A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
Theorem	dff1o4 6776	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 6777	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 6778	A one-to-one function maps onto its range. (Contributed by NM, 13-Aug-2004.)
⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
Theorem	f1f1orn 6779	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 6780	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 6781	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 6782	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 6783	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 6784	Preimage of an image. (Contributed by NM, 30-Sep-2004.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (◡𝐹 “ (𝐹 “ 𝐶)) = 𝐶)
Theorem	foimacnv 6785	A reverse version of f1imacnv 6784. (Contributed by Jeff Hankins, 16-Jul-2009.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶)
Theorem	foun 6786	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 6787	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 6788	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 6789	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 6790	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 6791	Composition of one-to-one onto functions. (Contributed by NM, 19-Mar-1998.)
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝐺:𝐴–1-1-onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1-onto→𝐶)
Theorem	f1cnv 6792	The converse of an injective function is bijective. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴–1-1→𝐵 → ◡𝐹:ran 𝐹–1-1-onto→𝐴)
Theorem	funcocnv2 6793	Composition with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹))
Theorem	fococnv2 6794	The composition of an onto function and its converse. (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
Theorem	f1ococnv2 6795	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 6796	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹))
Theorem	f1ococnv1 6797	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 6798	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴–1-1→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
Theorem	funcoeqres 6799	Express a constraint on a composition as a constraint on the composand. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ ((Fun 𝐺 ∧ (𝐹 ∘ 𝐺) = 𝐻) → (𝐹 ↾ ran 𝐺) = (𝐻 ∘ ◡𝐺))
Theorem	f1ssf1 6800	A subset of an injective function is injective. (Contributed by AV, 20-Nov-2020.)
⊢ ((Fun 𝐹 ∧ Fun ◡𝐹 ∧ 𝐺 ⊆ 𝐹) → Fun ◡𝐺)