Type  Label  Description 
Statement 

Theorem  funcnvres 5201 
The converse of a restricted function. (Contributed by set.mm
contributors, 27Mar1998.)

⊢ (Fun ^{◡}F
→ ^{◡}(F ↾ A) = (^{◡}F ↾ (F “
A))) 

Theorem  cnvresid 5202 
Converse of a restricted identity function. (Contributed by FL,
4Mar2007.)

⊢ ^{◡}( I
↾ A) =
( I ↾ A) 

Theorem  funcnvres2 5203 
The converse of a restriction of the converse of a function equals the
function restricted to the image of its converse. (Contributed by set.mm
contributors, 4May2005.)

⊢ (Fun F
→ ^{◡}(^{◡}F ↾ A) =
(F ↾
(^{◡}F “ A))) 

Theorem  funimacnv 5204 
The image of the preimage of a function. (Contributed by set.mm
contributors, 25May2004.)

⊢ (Fun F
→ (F “ (^{◡}F
“ A)) = (A ∩ ran F)) 

Theorem  funimass1 5205 
A kind of contraposition law that infers a subclass of an image from a
preimage subclass. (Contributed by set.mm contributors, 25May2004.)

⊢ ((Fun F
∧ A ⊆ ran F)
→ ((^{◡}F “ A)
⊆ B
→ A ⊆ (F “
B))) 

Theorem  funimass2 5206 
A kind of contraposition law that infers an image subclass from a subclass
of a preimage. (Contributed by set.mm contributors, 25May2004.)
(Revised by set.mm contributors, 4May2007.)

⊢ ((Fun F
∧ A ⊆ (^{◡}F
“ B)) → (F “ A)
⊆ B) 

Theorem  imadif 5207 
The image of a difference is the difference of images. (Contributed by
NM, 24May1998.)

⊢ (Fun ^{◡}F
→ (F “ (A ∖ B)) = ((F
“ A) ∖ (F “
B))) 

Theorem  imain 5208 
The image of an intersection is the intersection of images. (Contributed
by Paul Chapman, 11Apr2009.)

⊢ (Fun ^{◡}F
→ (F “ (A ∩ B)) =
((F “ A) ∩ (F
“ B))) 

Theorem  fneq1 5209 
Equality theorem for function predicate with domain. (Contributed by
set.mm contributors, 1Aug1994.)

⊢ (F =
G → (F Fn A ↔
G Fn A)) 

Theorem  fneq2 5210 
Equality theorem for function predicate with domain. (Contributed by
set.mm contributors, 1Aug1994.)

⊢ (A =
B → (F Fn A ↔
F Fn B)) 

Theorem  fneq1d 5211 
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22Jun2011.)

⊢ (φ
→ F = G) ⇒ ⊢ (φ
→ (F Fn A ↔ G Fn
A)) 

Theorem  fneq2d 5212 
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22Jun2011.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (F Fn A ↔ F Fn
B)) 

Theorem  fneq12d 5213 
Equality deduction for function predicate with domain. (Contributed by
set.mm contributors, 26Jun2011.)

⊢ (φ
→ F = G)
& ⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (F Fn A ↔ G Fn
B)) 

Theorem  fneq1i 5214 
Equality inference for function predicate with domain. (Contributed by
Paul Chapman, 22Jun2011.)

⊢ F =
G ⇒ ⊢ (F Fn
A ↔ G Fn A) 

Theorem  fneq2i 5215 
Equality inference for function predicate with domain. (Contributed by
set.mm contributors, 4Sep2011.)

⊢ A =
B ⇒ ⊢ (F Fn
A ↔ F Fn B) 

Theorem  nffn 5216 
Boundvariable hypothesis builder for a function with domain.
(Contributed by NM, 30Jan2004.)

⊢ F/_xF & ⊢ F/_xA ⇒ ⊢ Ⅎx
F Fn A 

Theorem  fnfun 5217 
A function with domain is a function. (Contributed by set.mm
contributors, 1Aug1994.)

⊢ (F Fn
A → Fun F) 

Theorem  fnrel 5218 
A function with domain is a relation. (Contributed by set.mm
contributors, 1Aug1994.)

⊢ (F Fn
A → Rel F) 

Theorem  fndm 5219 
The domain of a function. (Contributed by set.mm contributors,
2Aug1994.)

⊢ (F Fn
A → dom F = A) 

Theorem  funfni 5220 
Inference to convert a function and domain antecedent. (Contributed by
set.mm contributors, 22Apr2004.)

⊢ ((Fun F
∧ B ∈ dom F)
→ φ)
⇒ ⊢ ((F Fn A ∧ B ∈ A) →
φ) 

Theorem  fndmu 5221 
A function has a unique domain. (Contributed by set.mm contributors,
11Aug1994.)

⊢ ((F Fn
A ∧
F Fn B) → A =
B) 

Theorem  fnbr 5222 
The first argument of binary relation on a function belongs to the
function's domain. (Contributed by set.mm contributors, 7May2004.)

⊢ ((F Fn
A ∧
BFC) →
B ∈
A) 

Theorem  fnop 5223 
The first argument of an ordered pair in a function belongs to the
function's domain. (Contributed by set.mm contributors, 8Aug1994.)
(Revised by set.mm contributors, 25Mar2007.)

⊢ ((F Fn
A ∧ ⟨B, C⟩ ∈ F) →
B ∈
A) 

Theorem  fneu 5224* 
There is exactly one value of a function. (The proof was shortened by
Andrew Salmon, 17Sep2011.) (Contributed by set.mm contributors,
22Apr2004.) (Revised by set.mm contributors, 18Sep2011.)

⊢ ((F Fn
A ∧
B ∈
A) → ∃!y BFy) 

Theorem  fneu2 5225* 
There is exactly one value of a function. (Contributed by set.mm
contributors, 7Nov1995.)

⊢ ((F Fn
A ∧
B ∈
A) → ∃!y⟨B, y⟩ ∈ F) 

Theorem  fnun 5226 
The union of two functions with disjoint domains. (Contributed by set.mm
contributors, 22Sep2004.)

⊢ (((F Fn
A ∧
G Fn B) ∧ (A ∩ B) =
∅) → (F ∪ G) Fn
(A ∪ B)) 

Theorem  fnunsn 5227 
Extension of a function with a new ordered pair. (Contributed by NM,
28Sep2013.)

⊢ (φ
→ X ∈ V)
& ⊢ (φ
→ Y ∈ V)
& ⊢ (φ
→ F Fn D)
& ⊢ G =
(F ∪ {⟨X, Y⟩}) & ⊢ E =
(D ∪ {X})
& ⊢ (φ
→ ¬ X ∈ D) ⇒ ⊢ (φ
→ G Fn E) 

Theorem  fnco 5228 
Composition of two functions. (Contributed by set.mm contributors,
22May2006.)

⊢ ((F Fn
A ∧
G Fn B
∧ ran G
⊆ A)
→ (F ∘ G) Fn
B) 

Theorem  fnresdm 5229 
A function does not change when restricted to its domain. (Contributed by
set.mm contributors, 5Sep2004.)

⊢ (F Fn
A → (F ↾ A) = F) 

Theorem  fnresdisj 5230 
A function restricted to a class disjoint with its domain is empty.
(Contributed by set.mm contributors, 23Sep2004.)

⊢ (F Fn
A → ((A ∩ B) =
∅ ↔ (F ↾ B) = ∅)) 

Theorem  2elresin 5231 
Membership in two functions restricted by each other's domain.
(Contributed by set.mm contributors, 8Aug1994.)

⊢ ((F Fn
A ∧
G Fn B) → ((⟨x, y⟩ ∈ F ∧ ⟨x, z⟩ ∈ G) ↔ (⟨x, y⟩ ∈ (F ↾ (A ∩
B)) ∧
⟨x,
z⟩ ∈ (G ↾ (A ∩
B))))) 

Theorem  fnssresb 5232 
Restriction of a function with a subclass of its domain. (Contributed by
set.mm contributors, 10Oct2007.)

⊢ (F Fn
A → ((F ↾ B) Fn B ↔
B ⊆
A)) 

Theorem  fnssres 5233 
Restriction of a function with a subclass of its domain. (Contributed by
set.mm contributors, 2Aug1994.) (Revised by set.mm contributors,
25Sep2004.)

⊢ ((F Fn
A ∧
B ⊆
A) → (F ↾ B) Fn B) 

Theorem  fnresin1 5234 
Restriction of a function's domain with an intersection. (Contributed by
set.mm contributors, 9Aug1994.)

⊢ (F Fn
A → (F ↾ (A ∩ B)) Fn
(A ∩ B)) 

Theorem  fnresin2 5235 
Restriction of a function's domain with an intersection. (Contributed by
set.mm contributors, 9Aug1994.)

⊢ (F Fn
A → (F ↾ (B ∩ A)) Fn
(B ∩ A)) 

Theorem  fnres 5236* 
An equivalence for functionality of a restriction. Compare dffun8 5168.
(Contributed by Mario Carneiro, 20May2015.)

⊢ ((F ↾ A) Fn
A ↔ ∀x ∈ A ∃!y xFy) 

Theorem  fnresi 5237 
Functionality and domain of restricted identity. (Contributed by set.mm
contributors, 27Aug2004.)

⊢ ( I ↾
A) Fn A 

Theorem  fnima 5238 
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 5239 
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 5240 
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 5241* 
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 5242* 
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 5243* 
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 5244* 
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 5245* 
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 5246* 
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 5247 
Equality theorem for functions. (Contributed by set.mm contributors,
1Aug1994.)

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

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

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

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

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

Theorem  feq23 5250 
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 5251 
Equality deduction for functions. (Contributed by set.mm contributors,
19Feb2008.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ F/_xF & ⊢ F/_xA & ⊢ F/_xB ⇒ ⊢ Ⅎx
F:A–→B 

Theorem  elimf 5259 
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 5260 
A mapping is a function. (Contributed by set.mm contributors,
2Aug1994.)

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

Theorem  dffn2 5261 
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 5262 
A mapping is a function. (Contributed by set.mm contributors,
3Aug1994.)

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

Theorem  frel 5263 
A mapping is a relation. (Contributed by set.mm contributors,
3Aug1994.)

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

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

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

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

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

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

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

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

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

Theorem  fss 5268 
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 5269 
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 5270 
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 5271 
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 5272 
A mapping is a partial function. (Contributed by set.mm contributors,
25Nov2007.)

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

Theorem  opelf 5273 
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 5274 
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 5275 
Composition of two functions. (Contributed by set.mm contributors,
22May2006.)

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

Theorem  fssres 5276 
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 5277 
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 5278 
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 5279 
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 5280* 
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 5281 
The converse of a restriction of a function. (Contributed by set.mm
contributors, 26Mar1998.)

⊢ (F:A–→B
→ ^{◡}(F ↾ A) = (^{◡}F ↾ B)) 

Theorem  fimacnvdisj 5282 
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 5283* 
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 5284 
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 5285 
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 5286 
The empty function. (Contributed by set.mm contributors, 14Aug1999.)

⊢ ∅:∅–→A 

Theorem  f00 5287 
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 5288 
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 5289 
A cross product with a singleton is a constant function. (Contributed
by set.mm contributors, 19Oct2004.)

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

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

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

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

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

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

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

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

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

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

⊢ F/_xF & ⊢ F/_xA & ⊢ F/_xB ⇒ ⊢ Ⅎx
F:A–11→B 

Theorem  dff12 5295* 
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 5296 
A onetoone mapping is a mapping. (Contributed by set.mm contributors,
31Dec1996.)

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

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

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

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

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

Theorem  f1rel 5299 
A onetoone onto mapping is a relation. (Contributed by set.mm
contributors, 8Mar2014.)

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

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

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