Type  Label  Description 
Statement 

Theorem  fnima 5201 
The image of a function's domain is its range. (The proof was shortened
by Andrew Salmon, 17Sep2011.) (Contributed by set.mm contributors,
4Nov2004.) (Revised by set.mm contributors, 18Sep2011.)

⊢ (F Fn
A → (F “ A) =
ran F) 

Theorem  fn0 5202 
A function with empty domain is empty. (The proof was shortened by Andrew
Salmon, 17Sep2011.) (Contributed by set.mm contributors, 15Apr1998.)
(Revised by set.mm contributors, 18Sep2011.)

⊢ (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, 24Jan2007.)

⊢ ((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, 17Sep2011.) (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19Sep2011.)
(Contributed by set.mm contributors, 19Dec2008.)

⊢ B ∈ V ⇒ ⊢ ∪x ∈ A {⟨x, B⟩} = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)} 

Theorem  fnopabg 5205* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by NM, 30Jan2004.) (Proof shortened by Mario Carneiro,
4Dec2016.)

⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ φ)} ⇒ ⊢ (∀x ∈ A ∃!yφ ↔
F Fn A) 

Theorem  fnopab2g 5206* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by set.mm contributors, 23Mar2006.)

⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)} ⇒ ⊢ (∀x ∈ A B ∈ V ↔ F
Fn A) 

Theorem  fnopab 5207* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by set.mm contributors, 5Mar1996.)

⊢ (x ∈ A →
∃!yφ)
& ⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ φ)} ⇒ ⊢ F Fn
A 

Theorem  fnopab2 5208* 
Functionality and domain of an orderedpair class abstraction.
(Contributed by set.mm contributors, 29Jan2004.)

⊢ B ∈ V
& ⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)} ⇒ ⊢ F Fn
A 

Theorem  dmopab2 5209* 
Domain of an orderedpair class abstraction that specifies a function.
(Contributed by set.mm contributors, 6Sep2005.)

⊢ B ∈ V
& ⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)} ⇒ ⊢ dom F =
A 

Theorem  feq1 5210 
Equality theorem for functions. (Contributed by set.mm contributors,
1Aug1994.)

⊢ (F =
G → (F:A–→B
↔ G:A–→B)) 

Theorem  feq2 5211 
Equality theorem for functions. (Contributed by set.mm contributors,
1Aug1994.)

⊢ (A =
B → (F:A–→C
↔ F:B–→C)) 

Theorem  feq3 5212 
Equality theorem for functions. (Contributed by set.mm contributors,
1Aug1994.)

⊢ (A =
B → (F:C–→A
↔ F:C–→B)) 

Theorem  feq23 5213 
Equality theorem for functions. (Contributed by FL, 14Jul2007.) (The
proof was shortened by Andrew Salmon, 17Sep2011.)

⊢ ((A =
C ∧
B = D)
→ (F:A–→B
↔ F:C–→D)) 

Theorem  feq1d 5214 
Equality deduction for functions. (Contributed by set.mm contributors,
19Feb2008.)

⊢ (φ
→ F = G) ⇒ ⊢ (φ
→ (F:A–→B
↔ G:A–→B)) 

Theorem  feq2d 5215 
Equality deduction for functions. (Contributed by Paul Chapman,
22Jun2011.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (F:A–→C
↔ F:B–→C)) 

Theorem  feq12d 5216 
Equality deduction for functions. (Contributed by Paul Chapman,
22Jun2011.)

⊢ (φ
→ F = G)
& ⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (F:A–→C
↔ G:B–→C)) 

Theorem  feq1i 5217 
Equality inference for functions. (Contributed by Paul Chapman,
22Jun2011.)

⊢ F =
G ⇒ ⊢ (F:A–→B
↔ G:A–→B) 

Theorem  feq2i 5218 
Equality inference for functions. (Contributed by set.mm contributors,
5Sep2011.)

⊢ A =
B ⇒ ⊢ (F:A–→C
↔ F:B–→C) 

Theorem  feq23i 5219 
Equality inference for functions. (Contributed by Paul Chapman,
22Jun2011.)

⊢ A =
C
& ⊢ B =
D ⇒ ⊢ (F:A–→B
↔ F:C–→D) 

Theorem  feq23d 5220 
Equality deduction for functions. (Contributed by set.mm contributors,
8Jun2013.)

⊢ (φ
→ A = C)
& ⊢ (φ
→ B = D) ⇒ ⊢ (φ
→ (F:A–→B
↔ F:C–→D)) 

Theorem  nff 5221 
Boundvariable hypothesis builder for a mapping. (Contributed by NM,
29Jan2004.) (Revised by Mario Carneiro, 15Oct2016.)

⊢ Ⅎ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, 24Aug2006.)

⊢ G:A–→B ⇒ ⊢ if(F:A–→B, F, G):A–→B 

Theorem  ffn 5223 
A mapping is a function. (Contributed by set.mm contributors,
2Aug1994.)

⊢ (F:A–→B
→ F Fn A) 

Theorem  dffn2 5224 
Any function is a mapping into V. (The proof was shortened by
Andrew Salmon, 17Sep2011.) (Contributed by set.mm contributors,
31Oct1995.) (Revised by set.mm contributors, 18Sep2011.)

⊢ (F Fn
A ↔ F:A–→V) 

Theorem  ffun 5225 
A mapping is a function. (Contributed by set.mm contributors,
3Aug1994.)

⊢ (F:A–→B
→ Fun F) 

Theorem  fdm 5226 
The domain of a mapping. (Contributed by set.mm contributors,
2Aug1994.)

⊢ (F:A–→B
→ dom F = A) 

Theorem  fdmi 5227 
The domain of a mapping. (Contributed by set.mm contributors,
28Jul2008.)

⊢ F:A–→B ⇒ ⊢ dom F =
A 

Theorem  frn 5228 
The range of a mapping. (Contributed by set.mm contributors,
3Aug1994.)

⊢ (F:A–→B
→ ran F ⊆ B) 

Theorem  dffn3 5229 
A function maps to its range. (Contributed by set.mm contributors,
1Sep1999.)

⊢ (F Fn
A ↔ F:A–→ran F) 

Theorem  fss 5230 
Expanding the codomain of a mapping. (The proof was shortened by Andrew
Salmon, 17Sep2011.) (Contributed by set.mm contributors, 10May1998.)
(Revised by set.mm contributors, 18Sep2011.)

⊢ ((F:A–→B
∧ B ⊆ C) →
F:A–→C) 

Theorem  fco 5231 
Composition of two mappings. (The proof was shortened by Andrew Salmon,
17Sep2011.) (Contributed by set.mm contributors, 29Aug1999.)
(Revised by set.mm contributors, 18Sep2011.)

⊢ ((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, 17Sep2011.) (Contributed by set.mm contributors, 3Aug1994.)
(Revised by set.mm contributors, 18Sep2011.)

⊢ (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, 13Nov2007.)

⊢ ((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,
25Nov2007.)

⊢ (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,
9Jan2015.)

⊢ ((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, 22Sep2004.)

⊢ (((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,
22May2006.)

⊢ ((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, 23Sep2004.)

⊢ ((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, 21Jul2005.)

⊢ (((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, 17Sep2011.) (Contributed by set.mm
contributors, 13Dec2003.) (Revised by set.mm contributors,
18Sep2011.)

⊢ (F:A–→B
→ (F ∘ ( I ↾
A)) = F) 

Theorem  fcoi2 5241 
Composition of restricted identity and a mapping. (The proof was
shortened by Andrew Salmon, 17Sep2011.) (Contributed by set.mm
contributors, 13Dec2003.) (Revised by set.mm contributors,
18Sep2011.)

⊢ (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, 10Dec2003.)

⊢ ((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, 26Mar1998.)

⊢ (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, 24Jan2007.)

⊢ ((F:A–→B
∧ (B
∩ C) = ∅) → (^{◡}F
“ C) = ∅) 

Theorem  fint 5245* 
Function into an intersection. (The proof was shortened by Andrew
Salmon, 17Sep2011.) (Contributed by set.mm contributors,
14Oct1999.) (Revised by set.mm contributors, 18Sep2011.)

⊢ B ≠
∅ ⇒ ⊢ (F:A–→∩B ↔ ∀x ∈ B F:A–→x) 

Theorem  fin 5246 
Mapping into an intersection. (The proof was shortened by Andrew Salmon,
17Sep2011.) (Contributed by set.mm contributors, 14Sep1999.)
(Revised by set.mm contributors, 18Sep2011.)

⊢ (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, 17Sep2011.) (Contributed by set.mm contributors,
27Aug2006.) (Revised by set.mm contributors, 18Sep2011.)

⊢ ((F ∈ C ∧ F:A–→B) → A
∈ V) 

Theorem  f0 5248 
The empty function. (Contributed by set.mm contributors, 14Aug1999.)

⊢ ∅:∅–→A 

Theorem  f00 5249 
A class is a function with empty codomain iff it and its domain are
empty. (Contributed by set.mm contributors, 10Dec2003.)

⊢ (F:A–→∅
↔ (F = ∅ ∧ A = ∅)) 

Theorem  fconst 5250 
A cross product with a singleton is a constant function. (The proof was
shortened by Andrew Salmon, 17Sep2011.) (Contributed by set.mm
contributors, 14Aug1999.) (Revised by set.mm contributors,
18Sep2011.)

⊢ B ∈ V ⇒ ⊢ (A ×
{B}):A–→{B} 

Theorem  fconstg 5251 
A cross product with a singleton is a constant function. (Contributed
by set.mm contributors, 19Oct2004.)

⊢ (B ∈ V →
(A × {B}):A–→{B}) 

Theorem  fnconstg 5252 
A cross product with a singleton is a constant function. (Contributed
by set.mm contributors, 24Jul2014.)

⊢ (B ∈ V →
(A × {B}) Fn A) 

Theorem  f1eq1 5253 
Equality theorem for onetoone functions. (Contributed by set.mm
contributors, 10Feb1997.)

⊢ (F =
G → (F:A–11→B
↔ G:A–11→B)) 

Theorem  f1eq2 5254 
Equality theorem for onetoone functions. (Contributed by set.mm
contributors, 10Feb1997.)

⊢ (A =
B → (F:A–11→C
↔ F:B–11→C)) 

Theorem  f1eq3 5255 
Equality theorem for onetoone functions. (Contributed by set.mm
contributors, 10Feb1997.)

⊢ (A =
B → (F:C–11→A
↔ F:C–11→B)) 

Theorem  nff1 5256 
Boundvariable hypothesis builder for a onetoone function.
(Contributed by NM, 16May2004.)

⊢ ℲxF & ⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx
F:A–11→B 

Theorem  dff12 5257* 
Alternate definition of a onetoone function. (Contributed by set.mm
contributors, 31Dec1996.) (Revised by set.mm contributors,
22Sep2004.)

⊢ (F:A–11→B ↔
(F:A–→B
∧ ∀y∃*x xFy)) 

Theorem  f1f 5258 
A onetoone mapping is a mapping. (Contributed by set.mm contributors,
31Dec1996.)

⊢ (F:A–11→B →
F:A–→B) 

Theorem  f1fn 5259 
A onetoone mapping is a function on its domain. (Contributed by set.mm
contributors, 8Mar2014.)

⊢ (F:A–11→B →
F Fn A) 

Theorem  f1fun 5260 
A onetoone mapping is a function. (Contributed by set.mm contributors,
8Mar2014.)

⊢ (F:A–11→B →
Fun F) 

Theorem  f1dm 5261 
The domain of a onetoone mapping. (Contributed by set.mm contributors,
8Mar2014.)

⊢ (F:A–11→B →
dom F = A) 

Theorem  f1ss 5262 
A function that is onetoone is also onetoone on some superset of its
range. (Contributed by Mario Carneiro, 12Jan2013.)

⊢ ((F:A–11→B
∧ B ⊆ C) →
F:A–11→C) 

Theorem  f1funfun 5263 
Two ways to express that a set A is onetoone. Each side is equivalent
to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation
"Un_{2} (A)" for onetoone. We
do not introduce a separate notation since we
rarely use it. (Contributed by set.mm contributors, 13Aug2004.)
(Revised
by Scott Fenton, 18Apr2021.)

⊢ (A:dom
A–11→V ↔ (Fun ^{◡}A ∧ Fun A)) 

Theorem  f1co 5264 
Composition of onetoone functions. Exercise 30 of [TakeutiZaring]
p. 25. (Contributed by set.mm contributors, 28May1998.)

⊢ ((F:B–11→C
∧ G:A–11→B)
→ (F ∘ G):A–11→C) 

Theorem  foeq1 5265 
Equality theorem for onto functions. (Contributed by set.mm contributors,
1Aug1994.)

⊢ (F =
G → (F:A–onto→B
↔ G:A–onto→B)) 

Theorem  foeq2 5266 
Equality theorem for onto functions. (Contributed by set.mm contributors,
1Aug1994.)

⊢ (A =
B → (F:A–onto→C
↔ F:B–onto→C)) 

Theorem  foeq3 5267 
Equality theorem for onto functions. (Contributed by set.mm contributors,
1Aug1994.)

⊢ (A =
B → (F:C–onto→A
↔ F:C–onto→B)) 

Theorem  nffo 5268 
Boundvariable hypothesis builder for an onto function. (Contributed by
NM, 16May2004.)

⊢ ℲxF & ⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx
F:A–onto→B 

Theorem  fof 5269 
An onto mapping is a mapping. (Contributed by set.mm contributors,
3Aug1994.)

⊢ (F:A–onto→B →
F:A–→B) 

Theorem  fofun 5270 
An onto mapping is a function. (Contributed by set.mm contributors,
29Mar2008.)

⊢ (F:A–onto→B →
Fun F) 

Theorem  fofn 5271 
An onto mapping is a function on its domain. (Contributed by set.mm
contributors, 16Dec2008.)

⊢ (F:A–onto→B →
F Fn A) 

Theorem  forn 5272 
The codomain of an onto function is its range. (Contributed by set.mm
contributors, 3Aug1994.)

⊢ (F:A–onto→B →
ran F = B) 

Theorem  dffo2 5273 
Alternate definition of an onto function. (Contributed by set.mm
contributors, 22Mar2006.)

⊢ (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, 29Nov2002.)

⊢ (F:A–onto→B →
(F “ A) = B) 

Theorem  dffn4 5275 
A function maps onto its range. (Contributed by set.mm contributors,
10May1998.)

⊢ (F Fn
A ↔ F:A–onto→ran F) 

Theorem  funforn 5276 
A function maps its domain onto its range. (Contributed by set.mm
contributors, 23Jul2004.)

⊢ (Fun A
↔ A:dom A–onto→ran A) 

Theorem  fodmrnu 5277 
An onto function has unique domain and range. (Contributed by set.mm
contributors, 5Nov2006.)

⊢ ((F:A–onto→B
∧ F:C–onto→D) → (A =
C ∧
B = D)) 

Theorem  fores 5278 
Restriction of a function. (Contributed by set.mm contributors,
4Mar1997.)

⊢ ((Fun F
∧ A ⊆ dom F)
→ (F ↾ A):A–onto→(F
“ A)) 

Theorem  foco 5279 
Composition of onto functions. (Contributed by set.mm contributors,
22Mar2006.)

⊢ ((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,
12Jan2007.)

⊢ ((F:A–→{B} ∧ F ≠ ∅) →
F:A–onto→{B}) 

Theorem  f1oeq1 5281 
Equality theorem for onetoone onto functions. (Contributed by set.mm
contributors, 10Feb1997.)

⊢ (F =
G → (F:A–11onto→B ↔
G:A–11onto→B)) 

Theorem  f1oeq2 5282 
Equality theorem for onetoone onto functions. (Contributed by set.mm
contributors, 10Feb1997.)

⊢ (A =
B → (F:A–11onto→C ↔
F:B–11onto→C)) 

Theorem  f1oeq3 5283 
Equality theorem for onetoone onto functions. (Contributed by set.mm
contributors, 10Feb1997.)

⊢ (A =
B → (F:C–11onto→A ↔
F:C–11onto→B)) 

Theorem  f1oeq23 5284 
Equality theorem for onetoone onto functions. (Contributed by FL,
14Jul2012.)

⊢ ((A =
B ∧
C = D)
→ (F:A–11onto→C ↔
F:B–11onto→D)) 

Theorem  nff1o 5285 
Boundvariable hypothesis builder for a onetoone onto function.
(Contributed by NM, 16May2004.)

⊢ ℲxF & ⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx
F:A–11onto→B 

Theorem  f1of1 5286 
A onetoone onto mapping is a onetoone mapping. (Contributed by set.mm
contributors, 12Dec2003.)

⊢ (F:A–11onto→B →
F:A–11→B) 

Theorem  f1of 5287 
A onetoone onto mapping is a mapping. (Contributed by set.mm
contributors, 12Dec2003.)

⊢ (F:A–11onto→B →
F:A–→B) 

Theorem  f1ofn 5288 
A onetoone onto mapping is function on its domain. (Contributed by
set.mm contributors, 12Dec2003.)

⊢ (F:A–11onto→B →
F Fn A) 

Theorem  f1ofun 5289 
A onetoone onto mapping is a function. (Contributed by set.mm
contributors, 12Dec2003.)

⊢ (F:A–11onto→B →
Fun F) 

Theorem  f1odm 5290 
The domain of a onetoone onto mapping. (Contributed by set.mm
contributors, 8Mar2014.)

⊢ (F:A–11onto→B →
dom F = A) 

Theorem  dff1o2 5291 
Alternate definition of onetoone onto function. (The proof was
shortened by Andrew Salmon, 22Oct2011.) (Contributed by set.mm
contributors, 10Feb1997.) (Revised by set.mm contributors,
22Oct2011.)

⊢ (F:A–11onto→B ↔
(F Fn A ∧ Fun ^{◡}F ∧ ran F =
B)) 

Theorem  dff1o3 5292 
Alternate definition of onetoone onto function. (The proof was
shortened by Andrew Salmon, 22Oct2011.) (Contributed by set.mm
contributors, 25Mar1998.) (Revised by set.mm contributors,
22Oct2011.)

⊢ (F:A–11onto→B ↔
(F:A–onto→B ∧ Fun ^{◡}F)) 

Theorem  f1ofo 5293 
A onetoone onto function is an onto function. (Contributed by set.mm
contributors, 28Apr2004.)

⊢ (F:A–11onto→B →
F:A–onto→B) 

Theorem  dff1o4 5294 
Alternate definition of onetoone onto function. (The proof was
shortened by Andrew Salmon, 22Oct2011.) (Contributed by set.mm
contributors, 25Mar1998.) (Revised by set.mm contributors,
22Oct2011.)

⊢ (F:A–11onto→B ↔
(F Fn A ∧ ^{◡}F Fn
B)) 

Theorem  dff1o5 5295 
Alternate definition of onetoone onto function. (The proof was
shortened by Andrew Salmon, 22Oct2011.) (Contributed by set.mm
contributors, 10Dec2003.) (Revised by set.mm contributors,
22Oct2011.)

⊢ (F:A–11onto→B ↔
(F:A–11→B ∧ ran F =
B)) 

Theorem  f1orn 5296 
A onetoone function maps onto its range. (Contributed by set.mm
contributors, 13Aug2004.)

⊢ (F:A–11onto→ran
F ↔ (F Fn A ∧ Fun ^{◡}F)) 

Theorem  f1f1orn 5297 
A onetoone function maps onetoone onto its range. (Contributed by
set.mm contributors, 4Sep2004.)

⊢ (F:A–11→B →
F:A–11onto→ran
F) 

Theorem  f1ocnvb 5298 
A class is a onetoone onto function iff its converse is a onetoone
onto function with domain and range interchanged. (Contributed by set.mm
contributors, 8Dec2003.) (Modified by Scott Fenton, 17Apr2021.)

⊢ (F:A–11onto→B ↔
^{◡}F:B–11onto→A) 

Theorem  f1ocnv 5299 
The converse of a onetoone onto function is also onetoone onto. (The
proof was shortened by Andrew Salmon, 22Oct2011.) (Contributed by
set.mm contributors, 11Feb1997.) (Revised by set.mm contributors,
22Oct2011.)

⊢ (F:A–11onto→B →
^{◡}F:B–11onto→A) 

Theorem  f1ores 5300 
The restriction of a onetoone function maps onetoone onto the image.
(Contributed by set.mm contributors, 25Mar1998.)

⊢ ((F:A–11→B
∧ C ⊆ A) →
(F ↾
C):C–11onto→(F
“ C)) 