Type  Label  Description 
Statement 

Theorem  f1orescnv 5301 
The converse of a onetooneonto restricted function. (Contributed by
Paul Chapman, 21Apr2008.)

⊢ ((Fun ^{◡}F ∧ (F ↾ R):R–11onto→P) →
(^{◡}F ↾ P):P–11onto→R) 

Theorem  f1imacnv 5302 
Preimage of an image. (Contributed by set.mm contributors,
30Sep2004.)

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

Theorem  foimacnv 5303 
A reverse version of f1imacnv 5302. (Contributed by Jeffrey Hankins,
16Jul2009.)

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

Theorem  f1oun 5304 
The union of two onetoone onto functions with disjoint domains and
ranges. (Contributed by set.mm contributors, 26Mar1998.)

⊢ (((F:A–11onto→B ∧ G:C–11onto→D) ∧ ((A ∩
C) = ∅
∧ (B
∩ D) = ∅)) → (F
∪ G):(A ∪ C)–11onto→(B ∪
D)) 

Theorem  fun11iun 5305* 
The union of a chain (with respect to inclusion) of onetoone functions
is a onetoone function. (Contributed by Mario Carneiro,
20May2013.) (Revised by Mario Carneiro, 24Jun2015.)

⊢ (x =
y → B = C)
& ⊢ B ∈ V ⇒ ⊢ (∀x ∈ A (B:D–11→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) →
∪x ∈ A B:∪x ∈ A D–11→S) 

Theorem  resdif 5306 
The restriction of a onetoone onto function to a difference maps onto
the difference of the images. (Contributed by Paul Chapman,
11Apr2009.)

⊢ ((Fun ^{◡}F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) →
(F ↾
(A ∖
B)):(A
∖ B)–11onto→(C ∖ D)) 

Theorem  resin 5307 
The restriction of a onetoone onto function to an intersection maps onto
the intersection of the images. (Contributed by Paul Chapman,
11Apr2009.)

⊢ ((Fun ^{◡}F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) →
(F ↾
(A ∩ B)):(A ∩
B)–11onto→(C ∩
D)) 

Theorem  f1oco 5308 
Composition of onetoone onto functions. (Contributed by set.mm
contributors, 19Mar1998.)

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

Theorem  f1ococnv2 5309 
The composition of a onetoone onto function and its converse equals the
identity relation restricted to the function's range. (Contributed by
set.mm contributors, 13Dec2003.)

⊢ (F:A–11onto→B →
(F ∘
^{◡}F) = ( I ↾
B)) 

Theorem  f1ococnv1 5310 
The composition of a onetoone onto function's converse and itself equals
the identity relation restricted to the function's domain. (Contributed
by set.mm contributors, 13Dec2003.)

⊢ (F:A–11onto→B →
(^{◡}F ∘ F) = ( I ↾
A)) 

Theorem  f1cnv 5311 
The converse of an injective function is bijective. (Contributed by FL,
11Nov2011.)

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

Theorem  f1cocnv1 5312 
Composition of an injective function with its converse. (Contributed by
FL, 11Nov2011.)

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

Theorem  f1cocnv2 5313 
Composition of an injective function with its converse. (Contributed by
FL, 11Nov2011.)

⊢ (F:A–11→B →
(F ∘
^{◡}F) = ( I ↾ ran
F)) 

Theorem  ffoss 5314* 
Relationship between a mapping and an onto mapping. Figure 38 of
[Enderton] p. 145. (Contributed by
set.mm contributors,
10May1998.)

⊢ F ∈ V ⇒ ⊢ (F:A–→B
↔ ∃x(F:A–onto→x ∧ x ⊆ B)) 

Theorem  f11o 5315* 
Relationship between onetoone and onetoone onto function.
(Contributed by set.mm contributors, 4Apr1998.)

⊢ F ∈ V ⇒ ⊢ (F:A–11→B ↔
∃x(F:A–11onto→x ∧ x ⊆ B)) 

Theorem  f10 5316 
The empty set maps onetoone into any class. (Contributed by set.mm
contributors, 7Apr1998.)

⊢ ∅:∅–11→A 

Theorem  f1o00 5317 
Onetoone onto mapping of the empty set. (Contributed by set.mm
contributors, 15Apr1998.)

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

Theorem  fo00 5318 
Onto mapping of the empty set. (Contributed by set.mm contributors,
22Mar2006.)

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

Theorem  f1o0 5319 
Onetoone onto mapping of the empty set. (Contributed by set.mm
contributors, 10Feb2004.) (Revised by set.mm contributors,
16Feb2004.)

⊢ ∅:∅–11onto→∅ 

Theorem  f1oi 5320 
A restriction of the identity relation is a onetoone onto function.
(The proof was shortened by Andrew Salmon, 22Oct2011.) (Contributed by
set.mm contributors, 30Apr1998.) (Revised by set.mm contributors,
22Oct2011.)

⊢ ( I ↾
A):A–11onto→A 

Theorem  f1ovi 5321 
The identity relation is a onetoone onto function on the universe.
(Contributed by set.mm contributors, 16May2004.)

⊢ I :V–11onto→V 

Theorem  f1osn 5322 
A singleton of an ordered pair is onetoone onto function. (The proof
was shortened by Andrew Salmon, 22Oct2011.) (Contributed by set.mm
contributors, 18May1998.) (Revised by set.mm contributors,
22Oct2011.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ {⟨A, B⟩}:{A}–11onto→{B} 

Theorem  f1osng 5323 
A singleton of an ordered pair is onetoone onto function.
(Contributed by Mario Carneiro, 12Jan2013.)

⊢ ((A ∈ V ∧ B ∈ W) →
{⟨A,
B⟩}:{A}–11onto→{B}) 

Theorem  fv2 5324* 
Alternate definition of function value. Definition 10.11 of [Quine]
p. 68. (The proof was shortened by Andrew Salmon, 17Sep2011.)
(Contributed by set.mm contributors, 30Apr2004.) (Revised by set.mm
contributors, 18Sep2011.)

⊢ (F
‘A) = ∪{x ∣ ∀y(AFy ↔
y = x)} 

Theorem  fvprc 5325 
A function's value at a proper class is the empty set. (Contributed by
set.mm contributors, 20May1998.)

⊢ (¬ A
∈ V → (F ‘A) =
∅) 

Theorem  elfv 5326* 
Membership in a function value. (Contributed by set.mm contributors,
30Apr2004.)

⊢ (A ∈ (F
‘B) ↔ ∃x(A ∈ x ∧ ∀y(BFy ↔ y =
x))) 

Theorem  fveq1 5327 
Equality theorem for function value. (Contributed by set.mm
contributors, 29Dec1996.)

⊢ (F =
G → (F ‘A) =
(G ‘A)) 

Theorem  fveq2 5328 
Equality theorem for function value. (Contributed by set.mm
contributors, 29Dec1996.)

⊢ (A =
B → (F ‘A) =
(F ‘B)) 

Theorem  fveq1i 5329 
Equality inference for function value. (Contributed by set.mm
contributors, 2Sep2003.)

⊢ F =
G ⇒ ⊢ (F
‘A) = (G ‘A) 

Theorem  fveq1d 5330 
Equality deduction for function value. (Contributed by set.mm
contributors, 2Sep2003.)

⊢ (φ
→ F = G) ⇒ ⊢ (φ
→ (F ‘A) = (G
‘A)) 

Theorem  fveq2i 5331 
Equality inference for function value. (Contributed by set.mm
contributors, 28Jul1999.)

⊢ A =
B ⇒ ⊢ (F
‘A) = (F ‘B) 

Theorem  fveq2d 5332 
Equality deduction for function value. (Contributed by set.mm
contributors, 29May1999.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (F ‘A) = (F
‘B)) 

Theorem  fveq12d 5333 
Equality deduction for function value. (Contributed by FL,
22Dec2008.)

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

Theorem  nffv 5334 
Boundvariable hypothesis builder for function value. (Contributed by
NM, 14Nov1995.) (Revised by Mario Carneiro, 15Oct2016.)

⊢ ℲxF & ⊢ ℲxA ⇒ ⊢ Ⅎx(F
‘A) 

Theorem  nffvd 5335 
Deduction version of boundvariable hypothesis builder nffv 5334.
(Contributed by NM, 10Nov2005.) (Revised by Mario Carneiro,
15Oct2016.)

⊢ (φ
→ ℲxF)
& ⊢ (φ
→ ℲxA) ⇒ ⊢ (φ
→ Ⅎx(F ‘A)) 

Theorem  csbfv12g 5336 
Move class substitution in and out of a function value. (Contributed by
NM, 11Nov2005.)

⊢ (A ∈ C →
[A / x](F
‘B) = ([A / x]F
‘[A / x]B)) 

Theorem  csbfv2g 5337* 
Move class substitution in and out of a function value. (Contributed by
NM, 10Nov2005.)

⊢ (A ∈ C →
[A / x](F
‘B) = (F ‘[A / x]B)) 

Theorem  csbfvg 5338* 
Substitution for a function value. (Contributed by NM, 1Jan2006.)

⊢ (A ∈ C →
[A / x](F
‘x) = (F ‘A)) 

Theorem  fvex 5339 
The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27.
(Contributed by set.mm contributors, 30Dec1996.)

⊢ (F
‘A) ∈ V 

Theorem  fvif 5340 
Move a conditional outside of a function. (Contributed by Jeff Madsen,
2Sep2009.)

⊢ (F ‘
if(φ, A, B)) =
if(φ, (F ‘A),
(F ‘B)) 

Theorem  fv3 5341* 
Alternate definition of the value of a function. Definition 6.11 of
[TakeutiZaring] p. 26.
(Contributed by NM, 30Apr2004.) (Revised by
Mario Carneiro, 31Aug2015.)

⊢ (F
‘A) = {x ∣ (∃y(x ∈ y ∧ AFy) ∧ ∃!y AFy)} 

Theorem  fvres 5342 
The value of a restricted function. (Contributed by set.mm
contributors, 2Aug1994.) (Revised by set.mm contributors,
16Feb2004.)

⊢ (A ∈ B →
((F ↾
B) ‘A) = (F
‘A)) 

Theorem  funssfv 5343 
The value of a member of the domain of a subclass of a function.
(Contributed by set.mm contributors, 15Aug1994.) (Revised by set.mm
contributors, 29May2007.)

⊢ ((Fun F
∧ G ⊆ F ∧ A ∈ dom G)
→ (F ‘A) = (G
‘A)) 

Theorem  tz6.121 5344* 
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed
by NM, 30Apr2004.)

⊢ ((AFB ∧ ∃!y AFy) →
(F ‘A) = B) 

Theorem  tz6.12 5345* 
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed
by NM, 10Jul1994.)

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

Theorem  tz6.122 5346* 
Function value when F is not
a function. Theorem 6.12(2) of
[TakeutiZaring] p. 27.
(Contributed by set.mm contributors,
30Apr2004.)

⊢ (¬ ∃!y AFy → (F
‘A) = ∅) 

Theorem  tz6.12c 5347* 
Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by
NM, 30Apr2004.)

⊢ (∃!y AFy →
((F ‘A) = B ↔
AFB)) 

Theorem  tz6.12i 5348 
Corollary of Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by
set.mm contributors, 30Apr2004.) (Revised by set.mm contributors,
6Apr2007.)

⊢ (B ≠
∅ → ((F ‘A) =
B → AFB)) 

Theorem  ndmfv 5349 
The value of a class outside its domain is the empty set. (Contributed
by set.mm contributors, 24Aug1995.)

⊢ (¬ A
∈ dom F
→ (F ‘A) = ∅) 

Theorem  ndmfvrcl 5350 
Reverse closure law for function with the empty set not in its domain.
(Contributed by set.mm contributors, 26Apr1996.)

⊢ dom F =
S
& ⊢ ¬ ∅
∈ S ⇒ ⊢ ((F
‘A) ∈ S →
A ∈
S) 

Theorem  elfvdm 5351 
If a function value has a member, the argument belongs to the domain.
(Contributed by set.mm contributors, 12Feb2007.)

⊢ (A ∈ (F
‘B) → B ∈ dom F) 

Theorem  nfvres 5352 
The value of a nonmember of a restriction is the empty set. (Contributed
by set.mm contributors, 13Nov1995.)

⊢ (¬ A
∈ B
→ ((F ↾ B)
‘A) = ∅) 

Theorem  nfunsn 5353 
If the restriction of a class to a singleton is not a function, its
value is the empty set. (Contributed by NM, 8Aug2010.) (Proof
shortened by Andrew Salmon, 22Oct2011.)

⊢ (¬ Fun (F ↾ {A}) → (F
‘A) = ∅) 

Theorem  fv01 5354 
Function value of the empty set. (Contributed by Stefan O'Rear,
26Nov2014.)

⊢ (∅
‘A) = ∅ 

Theorem  fveqres 5355 
Equal values imply equal values in a restriction. (Contributed by set.mm
contributors, 13Nov1995.)

⊢ ((F
‘A) = (G ‘A)
→ ((F ↾ B)
‘A) = ((G ↾ B) ‘A)) 

Theorem  funbrfv 5356 
The second argument of a binary relation on a function is the function's
value. (Contributed by NM, 30Apr2004.) (Revised by Mario Carneiro,
28Apr2015.)

⊢ (Fun F
→ (AFB →
(F ‘A) = B)) 

Theorem  funopfv 5357 
The second element in an ordered pair member of a function is the
function's value. (Contributed by set.mm contributors, 19Jul1996.)

⊢ (Fun F
→ (⟨A, B⟩ ∈ F → (F
‘A) = B)) 

Theorem  fnbrfvb 5358 
Equivalence of function value and binary relation. (Contributed by NM,
19Apr2004.) (Revised by Mario Carneiro, 28Apr2015.)

⊢ ((F Fn
A ∧
B ∈
A) → ((F ‘B) =
C ↔ BFC)) 

Theorem  fnopfvb 5359 
Equivalence of function value and ordered pair membership. (Contributed
by set.mm contributors, 9Jan2015.)

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

Theorem  funbrfvb 5360 
Equivalence of function value and binary relation. (Contributed by set.mm
contributors, 9Jan2015.)

⊢ ((Fun F
∧ A ∈ dom F)
→ ((F ‘A) = B ↔
AFB)) 

Theorem  funopfvb 5361 
Equivalence of function value and ordered pair membership. Theorem
4.3(ii) of [Monk1] p. 42. (Contributed by
set.mm contributors,
9Jan2015.)

⊢ ((Fun F
∧ A ∈ dom F)
→ ((F ‘A) = B ↔
⟨A,
B⟩ ∈ F)) 

Theorem  funbrfv2b 5362 
Function value in terms of a binary relation. (Contributed by Mario
Carneiro, 19Mar2014.)

⊢ (Fun F
→ (AFB ↔
(A ∈ dom
F ∧
(F ‘A) = B))) 

Theorem  dffn5 5363* 
Representation of a function in terms of its values. (Contributed by
set.mm contributors, 29Jan2004.)

⊢ (F Fn
A ↔ F = {⟨x, y⟩ ∣ (x ∈ A ∧ y = (F
‘x))}) 

Theorem  fnrnfv 5364* 
The range of a function expressed as a collection of the function's
values. (Contributed by set.mm contributors, 20Oct2005.)

⊢ (F Fn
A → ran F = {y ∣ ∃x ∈ A y = (F ‘x)}) 

Theorem  fvelrnb 5365* 
A member of a function's range is a value of the function. (Contributed
by set.mm contributors, 31Oct1995.)

⊢ (F Fn
A → (B ∈ ran F ↔ ∃x ∈ A (F ‘x) =
B)) 

Theorem  dfimafn 5366* 
Alternate definition of the image of a function. (Contributed by Raph
Levien, 20Nov2006.)

⊢ ((Fun F
∧ A ⊆ dom F)
→ (F “ A) = {y ∣ ∃x ∈ A (F
‘x) = y}) 

Theorem  dfimafn2 5367* 
Alternate definition of the image of a function as an indexed union of
singletons of function values. (Contributed by Raph Levien,
20Nov2006.)

⊢ ((Fun F
∧ A ⊆ dom F)
→ (F “ A) = ∪x ∈ A {(F
‘x)}) 

Theorem  funimass4 5368* 
Membership relation for the values of a function whose image is a
subclass. (Contributed by Raph Levien, 20Nov2006.)

⊢ ((Fun F
∧ A ⊆ dom F)
→ ((F “ A) ⊆ B ↔ ∀x ∈ A (F ‘x)
∈ B)) 

Theorem  fvelima 5369* 
Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42.
(The proof was shortened by Andrew Salmon, 22Oct2011.) (Contributed
by set.mm contributors, 29Apr2004.) (Revised by set.mm contributors,
22Oct2011.)

⊢ ((Fun F
∧ A ∈ (F “
B)) → ∃x ∈ B (F ‘x) =
A) 

Theorem  fvelimab 5370* 
Function value in an image. (The proof was shortened by Andrew Salmon,
22Oct2011.) (An unnecessary distinct variable restriction was removed
by David Abernethy, 17Dec2011.) (Contributed by set.mm contributors,
20Jan2007.) (Revised by set.mm contributors, 25Dec2011.)

⊢ ((F Fn
A ∧
B ⊆
A) → (C ∈ (F “ B)
↔ ∃x ∈ B (F
‘x) = C)) 

Theorem  fniniseg 5371 
Membership in the preimage of a singleton, under a function. (Contributed
by Mario Carneiro, 12May2014.)

⊢ (F Fn
A → (C ∈ (^{◡}F
“ {B}) ↔ (C ∈ A ∧ (F ‘C) =
B))) 

Theorem  fniinfv 5372* 
The indexed intersection of a function's values is the intersection of
its range. (Contributed by set.mm contributors, 20Oct2005.)

⊢ (F Fn
A → ∩x ∈ A (F ‘x) =
∩ran F) 

Theorem  fnsnfv 5373 
Singleton of function value. (Contributed by set.mm contributors,
22May1998.)

⊢ ((F Fn
A ∧
B ∈
A) → {(F ‘B)} =
(F “ {B})) 

Theorem  fnimapr 5374 
The image of a pair under a funtion. (Contributed by Jeff Madsen,
6Jan2011.)

⊢ ((F Fn
A ∧
B ∈
A ∧
C ∈
A) → (F “ {B,
C}) = {(F ‘B),
(F ‘C)}) 

Theorem  funfv 5375 
A simplified expression for the value of a function when we know it's a
function. (Contributed by NM, 22May1998.)

⊢ (Fun F
→ (F ‘A) = ∪(F “ {A})) 

Theorem  funfv2 5376* 
The value of a function. Definition of function value in [Enderton]
p. 43. (Contributed by set.mm contributors, 22May1998.) (Revised by
set.mm contributors, 11May2005.)

⊢ (Fun F
→ (F ‘A) = ∪{y ∣ AFy}) 

Theorem  funfv2f 5377 
The value of a function. Version of funfv2 5376 using a boundvariable
hypotheses instead of distinct variable conditions. (Contributed by NM,
19Feb2006.)

⊢ ℲyA & ⊢ ℲyF ⇒ ⊢ (Fun F
→ (F ‘A) = ∪{y ∣ AFy}) 

Theorem  fvun 5378 
Value of the union of two functions when the domains are separate.
(Contributed by FL, 7Nov2011.)

⊢ (((Fun F
∧ Fun G)
∧ (dom F
∩ dom G) = ∅) → ((F
∪ G) ‘A) = ((F
‘A) ∪ (G ‘A))) 

Theorem  fvun1 5379 
The value of a union when the argument is in the first domain.
(Contributed by Scott Fenton, 29Jun2013.)

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

Theorem  fvun2 5380 
The value of a union when the argument is in the second domain.
(Contributed by Scott Fenton, 29Jun2013.)

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

Theorem  dmfco 5381 
Domains of a function composition. (Contributed by set.mm contributors,
27Jan1997.)

⊢ ((Fun G
∧ A ∈ dom G)
→ (A ∈ dom (F ∘ G) ↔
(G ‘A) ∈ dom F)) 

Theorem  fvco2 5382 
Value of a function composition. Similar to second part of Theorem 3H
of [Enderton] p. 47. (The proof was
shortened by Andrew Salmon,
22Oct2011.) (Contributed by set.mm contributors, 9Oct2004.)
(Revised by set.mm contributors, 22Oct2011.)

⊢ ((G Fn
A ∧
C ∈
A) → ((F ∘ G) ‘C) =
(F ‘(G ‘C))) 

Theorem  fvco 5383 
Value of a function composition. Similar to Exercise 5 of [TakeutiZaring]
p. 28. (Contributed by set.mm contributors, 22Apr2006.)

⊢ ((Fun G
∧ A ∈ dom G)
→ ((F ∘ G)
‘A) = (F ‘(G
‘A))) 

Theorem  fvco3 5384 
Value of a function composition. (Contributed by set.mm contributors,
3Jan2004.) (Revised by set.mm contributors, 21Aug2006.)

⊢ ((G:A–→B
∧ C ∈ A) →
((F ∘
G) ‘C) = (F
‘(G ‘C))) 

Theorem  fvopab4t 5385* 
Closed theorem form of fvopab4 5389. (Contributed by set.mm contributors,
21Feb2013.)

⊢ ((∀x∀y(x = A → B =
C) ∧
∀x
F = {⟨x, y⟩ ∣ (x ∈ D ∧ y = B)} ∧ (A ∈ D ∧ C ∈ V)) → (F
‘A) = C) 

Theorem  fvopab3g 5386* 
Value of a function given by orderedpair class abstraction.
(Contributed by set.mm contributors, 6Mar1996.)

⊢ B ∈ V
& ⊢ (x =
A → (φ ↔ ψ))
& ⊢ (y =
B → (ψ ↔ χ))
& ⊢ (x ∈ C →
∃!yφ)
& ⊢ F = {⟨x, y⟩ ∣ (x ∈ C ∧ φ)} ⇒ ⊢ (A ∈ C →
((F ‘A) = B ↔
χ)) 

Theorem  fvopab3ig 5387* 
Value of a function given by orderedpair class abstraction.
(Contributed by set.mm contributors, 23Oct1999.)

⊢ (x =
A → (φ ↔ ψ))
& ⊢ (y =
B → (ψ ↔ χ))
& ⊢ (x ∈ C →
∃*yφ)
& ⊢ F = {⟨x, y⟩ ∣ (x ∈ C ∧ φ)} ⇒ ⊢ ((A ∈ C ∧ B ∈ D) →
(χ → (F ‘A) =
B)) 

Theorem  fvopab4g 5388* 
Value of a function given by orderedpair class abstraction.
(Contributed by set.mm contributors, 23Oct1999.)

⊢ (x =
A → B = C)
& ⊢ F = {⟨x, y⟩ ∣ (x ∈ D ∧ y = B)} ⇒ ⊢ ((A ∈ D ∧ C ∈ R) →
(F ‘A) = C) 

Theorem  fvopab4 5389* 
Value of a function given by orderedpair class abstraction.
(Contributed by set.mm contributors, 23Oct1999.)

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

Theorem  fvopab4ndm 5390* 
Value of a function given by an orderedpair class abstraction, outside
of its domain. (Contributed by set.mm contributors, 28Mar2008.)

⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ φ)} ⇒ ⊢ (¬ B
∈ A
→ (F ‘B) = ∅) 

Theorem  fvopabg 5391* 
The value of a function given by orderedpair class abstraction.
(Contributed by set.mm contributors, 2Sep2003.)

⊢ (x =
A → B = C) ⇒ ⊢ ((A ∈ V ∧ C ∈ W) →
({⟨x,
y⟩ ∣ y =
B} ‘A) = C) 

Theorem  eqfnfv 5392* 
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
(The proof was shortened by Andrew Salmon, 22Oct2011.) (Contributed
by set.mm contributors, 3Aug1994.) (Revised by set.mm contributors,
22Oct2011.)

⊢ ((F Fn
A ∧
G Fn A) → (F =
G ↔ ∀x ∈ A (F ‘x) =
(G ‘x))) 

Theorem  eqfnfv2 5393* 
Equality of functions is determined by their values. Exercise 4 of
[TakeutiZaring] p. 28.
(Contributed by set.mm contributors,
3Aug1994.) (Revised by set.mm contributors, 5Feb2004.)

⊢ ((F Fn
A ∧
G Fn B) → (F =
G ↔ (A = B ∧ ∀x ∈ A (F
‘x) = (G ‘x)))) 

Theorem  eqfnfv3 5394* 
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2Sep2009.)

⊢ ((F Fn
A ∧
G Fn B) → (F =
G ↔ (B ⊆ A ∧ ∀x ∈ A (x ∈ B ∧ (F ‘x) =
(G ‘x))))) 

Theorem  eqfnfvd 5395* 
Deduction for equality of functions. (Contributed by Mario Carneiro,
24Jul2014.)

⊢ (φ
→ F Fn A)
& ⊢ (φ
→ G Fn A)
& ⊢ ((φ
∧ x ∈ A) →
(F ‘x) = (G
‘x)) ⇒ ⊢ (φ
→ F = G) 

Theorem  eqfnfv2f 5396* 
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
This version of eqfnfv 5392 uses boundvariable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29Jan2004.)

⊢ ℲxF & ⊢ ℲxG ⇒ ⊢ ((F Fn
A ∧
G Fn A) → (F =
G ↔ ∀x ∈ A (F ‘x) =
(G ‘x))) 

Theorem  eqfunfv 5397* 
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19Jun2011.)

⊢ ((Fun F
∧ Fun G)
→ (F = G ↔ (dom F
= dom G ∧
∀x
∈ dom F(F
‘x) = (G ‘x)))) 

Theorem  fvreseq 5398* 
Equality of restricted functions is determined by their values.
(Contributed by set.mm contributors, 3Aug1994.) (Revised by set.mm
contributors, 6Feb2004.)

⊢ (((F Fn
A ∧
G Fn A) ∧ B ⊆ A) → ((F
↾ B) =
(G ↾
B) ↔ ∀x ∈ B (F ‘x) =
(G ‘x))) 

Theorem  chfnrn 5399* 
The range of a choice function (a function that chooses an element from
each member of its domain) is included in the union of its domain.
(Contributed by set.mm contributors, 31Aug1999.)

⊢ ((F Fn
A ∧ ∀x ∈ A (F ‘x)
∈ x)
→ ran F ⊆ ∪A) 

Theorem  funfvop 5400 
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by set.mm contributors, 14Oct1996.)

⊢ ((Fun F
∧ A ∈ dom F)
→ ⟨A, (F
‘A)⟩ ∈ F) 