P. 53 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5201-5300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fnima 5201	The image of a function's domain is its range. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 4-Nov-2004.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ (F Fn A → (F “ A) = ran F)
Theorem	fn0 5202	A function with empty domain is empty. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 15-Apr-1998.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ (F Fn ∅ ↔ F = ∅)
Theorem	fnimadisj 5203	A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007.)
⊢ ((F Fn A ∧ (A ∩ C) = ∅) → (F “ C) = ∅)
Theorem	iunfopab 5204*	Two ways to express a function as a class of ordered pairs. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Sep-2011.) (Contributed by set.mm contributors, 19-Dec-2008.)
⊢ B ∈ V    ⇒   ⊢ ∪x ∈ A {⟨x, B⟩} = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}
Theorem	fnopabg 5205*	Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)
⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ φ)}    ⇒   ⊢ (∀x ∈ A ∃!yφ ↔ F Fn A)
Theorem	fnopab2g 5206*	Functionality and domain of an ordered-pair class abstraction. (Contributed by set.mm contributors, 23-Mar-2006.)
⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}    ⇒   ⊢ (∀x ∈ A B ∈ V ↔ F Fn A)
Theorem	fnopab 5207*	Functionality and domain of an ordered-pair class abstraction. (Contributed by set.mm contributors, 5-Mar-1996.)
⊢ (x ∈ A → ∃!yφ)    &   ⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ φ)}    ⇒   ⊢ F Fn A
Theorem	fnopab2 5208*	Functionality and domain of an ordered-pair class abstraction. (Contributed by set.mm contributors, 29-Jan-2004.)
⊢ B ∈ V    &   ⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}    ⇒   ⊢ F Fn A
Theorem	dmopab2 5209*	Domain of an ordered-pair class abstraction that specifies a function. (Contributed by set.mm contributors, 6-Sep-2005.)
⊢ B ∈ V    &   ⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}    ⇒   ⊢ dom F = A
Theorem	feq1 5210	Equality theorem for functions. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (F = G → (F:A–→B ↔ G:A–→B))
Theorem	feq2 5211	Equality theorem for functions. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (A = B → (F:A–→C ↔ F:B–→C))
Theorem	feq3 5212	Equality theorem for functions. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (A = B → (F:C–→A ↔ F:C–→B))
Theorem	feq23 5213	Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((A = C ∧ B = D) → (F:A–→B ↔ F:C–→D))
Theorem	feq1d 5214	Equality deduction for functions. (Contributed by set.mm contributors, 19-Feb-2008.)
⊢ (φ → F = G)    ⇒   ⊢ (φ → (F:A–→B ↔ G:A–→B))
Theorem	feq2d 5215	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (F:A–→C ↔ F:B–→C))
Theorem	feq12d 5216	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (φ → F = G)    &   ⊢ (φ → A = B)    ⇒   ⊢ (φ → (F:A–→C ↔ G:B–→C))
Theorem	feq1i 5217	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ F = G    ⇒   ⊢ (F:A–→B ↔ G:A–→B)
Theorem	feq2i 5218	Equality inference for functions. (Contributed by set.mm contributors, 5-Sep-2011.)
⊢ A = B    ⇒   ⊢ (F:A–→C ↔ F:B–→C)
Theorem	feq23i 5219	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ A = C    &   ⊢ B = D    ⇒   ⊢ (F:A–→B ↔ F:C–→D)
Theorem	feq23d 5220	Equality deduction for functions. (Contributed by set.mm contributors, 8-Jun-2013.)
⊢ (φ → A = C)    &   ⊢ (φ → B = D)    ⇒   ⊢ (φ → (F:A–→B ↔ F:C–→D))
Theorem	nff 5221	Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ ℲxF    &   ⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx F:A–→B
Theorem	elimf 5222	Eliminate a mapping hypothesis for the weak deduction theorem dedth 3703, when a special case G:A–→B is provable, in order to convert F:A–→B from a hypothesis to an antecedent. (Contributed by set.mm contributors, 24-Aug-2006.)
⊢ G:A–→B    ⇒   ⊢ if(F:A–→B, F, G):A–→B
Theorem	ffn 5223	A mapping is a function. (Contributed by set.mm contributors, 2-Aug-1994.)
⊢ (F:A–→B → F Fn A)
Theorem	dffn2 5224	Any function is a mapping into V. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 31-Oct-1995.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ (F Fn A ↔ F:A–→V)
Theorem	ffun 5225	A mapping is a function. (Contributed by set.mm contributors, 3-Aug-1994.)
⊢ (F:A–→B → Fun F)
Theorem	fdm 5226	The domain of a mapping. (Contributed by set.mm contributors, 2-Aug-1994.)
⊢ (F:A–→B → dom F = A)
Theorem	fdmi 5227	The domain of a mapping. (Contributed by set.mm contributors, 28-Jul-2008.)
⊢ F:A–→B    ⇒   ⊢ dom F = A
Theorem	frn 5228	The range of a mapping. (Contributed by set.mm contributors, 3-Aug-1994.)
⊢ (F:A–→B → ran F ⊆ B)
Theorem	dffn3 5229	A function maps to its range. (Contributed by set.mm contributors, 1-Sep-1999.)
⊢ (F Fn A ↔ F:A–→ran F)
Theorem	fss 5230	Expanding the codomain of a mapping. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 10-May-1998.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ ((F:A–→B ∧ B ⊆ C) → F:A–→C)
Theorem	fco 5231	Composition of two mappings. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 29-Aug-1999.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ ((F:B–→C ∧ G:A–→B) → (F ∘ G):A–→C)
Theorem	fssxp 5232	A mapping is a class of ordered pairs. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 3-Aug-1994.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ (F:A–→B → F ⊆ (A × B))
Theorem	funssxp 5233	Two ways of specifying a partial function from A to B. (Contributed by set.mm contributors, 13-Nov-2007.)
⊢ ((Fun F ∧ F ⊆ (A × B)) ↔ (F:dom F–→B ∧ dom F ⊆ A))
Theorem	ffdm 5234	A mapping is a partial function. (Contributed by set.mm contributors, 25-Nov-2007.)
⊢ (F:A–→B → (F:dom F–→B ∧ dom F ⊆ A))
Theorem	opelf 5235	The members of an ordered pair element of a mapping belong to the mapping's domain and codomain. (Contributed by set.mm contributors, 9-Jan-2015.)
⊢ ((F:A–→B ∧ ⟨C, D⟩ ∈ F) → (C ∈ A ∧ D ∈ B))
Theorem	fun 5236	The union of two functions with disjoint domains. (Contributed by set.mm contributors, 22-Sep-2004.)
⊢ (((F:A–→C ∧ G:B–→D) ∧ (A ∩ B) = ∅) → (F ∪ G):(A ∪ B)–→(C ∪ D))
Theorem	fnfco 5237	Composition of two functions. (Contributed by set.mm contributors, 22-May-2006.)
⊢ ((F Fn A ∧ G:B–→A) → (F ∘ G) Fn B)
Theorem	fssres 5238	Restriction of a function with a subclass of its domain. (Contributed by set.mm contributors, 23-Sep-2004.)
⊢ ((F:A–→B ∧ C ⊆ A) → (F ↾ C):C–→B)
Theorem	fssres2 5239	Restriction of a restricted function with a subclass of its domain. (Contributed by set.mm contributors, 21-Jul-2005.)
⊢ (((F ↾ A):A–→B ∧ C ⊆ A) → (F ↾ C):C–→B)
Theorem	fcoi1 5240	Composition of a mapping and restricted identity. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 13-Dec-2003.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ (F:A–→B → (F ∘ ( I ↾ A)) = F)
Theorem	fcoi2 5241	Composition of restricted identity and a mapping. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 13-Dec-2003.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ (F:A–→B → (( I ↾ B) ∘ F) = F)
Theorem	feu 5242*	There is exactly one value of a function in its codomain. (Contributed by set.mm contributors, 10-Dec-2003.)
⊢ ((F:A–→B ∧ C ∈ A) → ∃!y ∈ B ⟨C, y⟩ ∈ F)
Theorem	fcnvres 5243	The converse of a restriction of a function. (Contributed by set.mm contributors, 26-Mar-1998.)
⊢ (F:A–→B → ◡(F ↾ A) = (◡F ↾ B))
Theorem	fimacnvdisj 5244	The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007.)
⊢ ((F:A–→B ∧ (B ∩ C) = ∅) → (◡F “ C) = ∅)
Theorem	fint 5245*	Function into an intersection. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 14-Oct-1999.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ B ≠ ∅    ⇒   ⊢ (F:A–→∩B ↔ ∀x ∈ B F:A–→x)
Theorem	fin 5246	Mapping into an intersection. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 14-Sep-1999.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ (F:A–→(B ∩ C) ↔ (F:A–→B ∧ F:A–→C))
Theorem	dmfex 5247	If a mapping is a set, its domain is a set. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 27-Aug-2006.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ ((F ∈ C ∧ F:A–→B) → A ∈ V)
Theorem	f0 5248	The empty function. (Contributed by set.mm contributors, 14-Aug-1999.)
⊢ ∅:∅–→A
Theorem	f00 5249	A class is a function with empty codomain iff it and its domain are empty. (Contributed by set.mm contributors, 10-Dec-2003.)
⊢ (F:A–→∅ ↔ (F = ∅ ∧ A = ∅))
Theorem	fconst 5250	A cross product with a singleton is a constant function. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 14-Aug-1999.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ B ∈ V    ⇒   ⊢ (A × {B}):A–→{B}
Theorem	fconstg 5251	A cross product with a singleton is a constant function. (Contributed by set.mm contributors, 19-Oct-2004.)
⊢ (B ∈ V → (A × {B}):A–→{B})
Theorem	fnconstg 5252	A cross product with a singleton is a constant function. (Contributed by set.mm contributors, 24-Jul-2014.)
⊢ (B ∈ V → (A × {B}) Fn A)
Theorem	f1eq1 5253	Equality theorem for one-to-one functions. (Contributed by set.mm contributors, 10-Feb-1997.)
⊢ (F = G → (F:A–1-1→B ↔ G:A–1-1→B))
Theorem	f1eq2 5254	Equality theorem for one-to-one functions. (Contributed by set.mm contributors, 10-Feb-1997.)
⊢ (A = B → (F:A–1-1→C ↔ F:B–1-1→C))
Theorem	f1eq3 5255	Equality theorem for one-to-one functions. (Contributed by set.mm contributors, 10-Feb-1997.)
⊢ (A = B → (F:C–1-1→A ↔ F:C–1-1→B))
Theorem	nff1 5256	Bound-variable hypothesis builder for a one-to-one function. (Contributed by NM, 16-May-2004.)
⊢ ℲxF    &   ⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx F:A–1-1→B
Theorem	dff12 5257*	Alternate definition of a one-to-one function. (Contributed by set.mm contributors, 31-Dec-1996.) (Revised by set.mm contributors, 22-Sep-2004.)
⊢ (F:A–1-1→B ↔ (F:A–→B ∧ ∀y∃*x xFy))
Theorem	f1f 5258	A one-to-one mapping is a mapping. (Contributed by set.mm contributors, 31-Dec-1996.)
⊢ (F:A–1-1→B → F:A–→B)
Theorem	f1fn 5259	A one-to-one mapping is a function on its domain. (Contributed by set.mm contributors, 8-Mar-2014.)
⊢ (F:A–1-1→B → F Fn A)
Theorem	f1fun 5260	A one-to-one mapping is a function. (Contributed by set.mm contributors, 8-Mar-2014.)
⊢ (F:A–1-1→B → Fun F)
Theorem	f1dm 5261	The domain of a one-to-one mapping. (Contributed by set.mm contributors, 8-Mar-2014.)
⊢ (F:A–1-1→B → dom F = A)
Theorem	f1ss 5262	A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Mario Carneiro, 12-Jan-2013.)
⊢ ((F:A–1-1→B ∧ B ⊆ C) → F:A–1-1→C)
Theorem	f1funfun 5263	Two ways to express that a set A 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 set.mm contributors, 13-Aug-2004.) (Revised by Scott Fenton, 18-Apr-2021.)
⊢ (A:dom A–1-1→V ↔ (Fun ◡A ∧ Fun A))
Theorem	f1co 5264	Composition of one-to-one functions. Exercise 30 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 28-May-1998.)
⊢ ((F:B–1-1→C ∧ G:A–1-1→B) → (F ∘ G):A–1-1→C)
Theorem	foeq1 5265	Equality theorem for onto functions. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (F = G → (F:A–onto→B ↔ G:A–onto→B))
Theorem	foeq2 5266	Equality theorem for onto functions. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (A = B → (F:A–onto→C ↔ F:B–onto→C))
Theorem	foeq3 5267	Equality theorem for onto functions. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (A = B → (F:C–onto→A ↔ F:C–onto→B))
Theorem	nffo 5268	Bound-variable hypothesis builder for an onto function. (Contributed by NM, 16-May-2004.)
⊢ ℲxF    &   ⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx F:A–onto→B
Theorem	fof 5269	An onto mapping is a mapping. (Contributed by set.mm contributors, 3-Aug-1994.)
⊢ (F:A–onto→B → F:A–→B)
Theorem	fofun 5270	An onto mapping is a function. (Contributed by set.mm contributors, 29-Mar-2008.)
⊢ (F:A–onto→B → Fun F)
Theorem	fofn 5271	An onto mapping is a function on its domain. (Contributed by set.mm contributors, 16-Dec-2008.)
⊢ (F:A–onto→B → F Fn A)
Theorem	forn 5272	The codomain of an onto function is its range. (Contributed by set.mm contributors, 3-Aug-1994.)
⊢ (F:A–onto→B → ran F = B)
Theorem	dffo2 5273	Alternate definition of an onto function. (Contributed by set.mm contributors, 22-Mar-2006.)
⊢ (F:A–onto→B ↔ (F:A–→B ∧ ran F = B))
Theorem	foima 5274	The image of the domain of an onto function. (Contributed by set.mm contributors, 29-Nov-2002.)
⊢ (F:A–onto→B → (F “ A) = B)
Theorem	dffn4 5275	A function maps onto its range. (Contributed by set.mm contributors, 10-May-1998.)
⊢ (F Fn A ↔ F:A–onto→ran F)
Theorem	funforn 5276	A function maps its domain onto its range. (Contributed by set.mm contributors, 23-Jul-2004.)
⊢ (Fun A ↔ A:dom A–onto→ran A)
Theorem	fodmrnu 5277	An onto function has unique domain and range. (Contributed by set.mm contributors, 5-Nov-2006.)
⊢ ((F:A–onto→B ∧ F:C–onto→D) → (A = C ∧ B = D))
Theorem	fores 5278	Restriction of a function. (Contributed by set.mm contributors, 4-Mar-1997.)
⊢ ((Fun F ∧ A ⊆ dom F) → (F ↾ A):A–onto→(F “ A))
Theorem	foco 5279	Composition of onto functions. (Contributed by set.mm contributors, 22-Mar-2006.)
⊢ ((F:B–onto→C ∧ G:A–onto→B) → (F ∘ G):A–onto→C)
Theorem	foconst 5280	A nonzero constant function is onto. (Contributed by set.mm contributors, 12-Jan-2007.)
⊢ ((F:A–→{B} ∧ F ≠ ∅) → F:A–onto→{B})
Theorem	f1oeq1 5281	Equality theorem for one-to-one onto functions. (Contributed by set.mm contributors, 10-Feb-1997.)
⊢ (F = G → (F:A–1-1-onto→B ↔ G:A–1-1-onto→B))
Theorem	f1oeq2 5282	Equality theorem for one-to-one onto functions. (Contributed by set.mm contributors, 10-Feb-1997.)
⊢ (A = B → (F:A–1-1-onto→C ↔ F:B–1-1-onto→C))
Theorem	f1oeq3 5283	Equality theorem for one-to-one onto functions. (Contributed by set.mm contributors, 10-Feb-1997.)
⊢ (A = B → (F:C–1-1-onto→A ↔ F:C–1-1-onto→B))
Theorem	f1oeq23 5284	Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.)
⊢ ((A = B ∧ C = D) → (F:A–1-1-onto→C ↔ F:B–1-1-onto→D))
Theorem	nff1o 5285	Bound-variable hypothesis builder for a one-to-one onto function. (Contributed by NM, 16-May-2004.)
⊢ ℲxF    &   ⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx F:A–1-1-onto→B
Theorem	f1of1 5286	A one-to-one onto mapping is a one-to-one mapping. (Contributed by set.mm contributors, 12-Dec-2003.)
⊢ (F:A–1-1-onto→B → F:A–1-1→B)
Theorem	f1of 5287	A one-to-one onto mapping is a mapping. (Contributed by set.mm contributors, 12-Dec-2003.)
⊢ (F:A–1-1-onto→B → F:A–→B)
Theorem	f1ofn 5288	A one-to-one onto mapping is function on its domain. (Contributed by set.mm contributors, 12-Dec-2003.)
⊢ (F:A–1-1-onto→B → F Fn A)
Theorem	f1ofun 5289	A one-to-one onto mapping is a function. (Contributed by set.mm contributors, 12-Dec-2003.)
⊢ (F:A–1-1-onto→B → Fun F)
Theorem	f1odm 5290	The domain of a one-to-one onto mapping. (Contributed by set.mm contributors, 8-Mar-2014.)
⊢ (F:A–1-1-onto→B → dom F = A)
Theorem	dff1o2 5291	Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 10-Feb-1997.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ (F:A–1-1-onto→B ↔ (F Fn A ∧ Fun ◡F ∧ ran F = B))
Theorem	dff1o3 5292	Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 25-Mar-1998.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ (F:A–1-1-onto→B ↔ (F:A–onto→B ∧ Fun ◡F))
Theorem	f1ofo 5293	A one-to-one onto function is an onto function. (Contributed by set.mm contributors, 28-Apr-2004.)
⊢ (F:A–1-1-onto→B → F:A–onto→B)
Theorem	dff1o4 5294	Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 25-Mar-1998.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ (F:A–1-1-onto→B ↔ (F Fn A ∧ ◡F Fn B))
Theorem	dff1o5 5295	Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 10-Dec-2003.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ ran F = B))
Theorem	f1orn 5296	A one-to-one function maps onto its range. (Contributed by set.mm contributors, 13-Aug-2004.)
⊢ (F:A–1-1-onto→ran F ↔ (F Fn A ∧ Fun ◡F))
Theorem	f1f1orn 5297	A one-to-one function maps one-to-one onto its range. (Contributed by set.mm contributors, 4-Sep-2004.)
⊢ (F:A–1-1→B → F:A–1-1-onto→ran F)
Theorem	f1ocnvb 5298	A class is a one-to-one onto function iff its converse is a one-to-one onto function with domain and range interchanged. (Contributed by set.mm contributors, 8-Dec-2003.) (Modified by Scott Fenton, 17-Apr-2021.)
⊢ (F:A–1-1-onto→B ↔ ◡F:B–1-1-onto→A)
Theorem	f1ocnv 5299	The converse of a one-to-one onto function is also one-to-one onto. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 11-Feb-1997.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ (F:A–1-1-onto→B → ◡F:B–1-1-onto→A)
Theorem	f1ores 5300	The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by set.mm contributors, 25-Mar-1998.)
⊢ ((F:A–1-1→B ∧ C ⊆ A) → (F ↾ C):C–1-1-onto→(F “ C))