Type  Label  Description 
Statement 

Theorem  funopfvb 5401 
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 5402 
Function value in terms of a binary relation. (Contributed by Mario
Carneiro, 19Mar2014.)

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

Theorem  dffn5 5403* 
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 5404* 
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 5405* 
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 5406* 
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 5407* 
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 5408* 
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 5409* 
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 5410* 
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 5411 
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 5412* 
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 5413 
Singleton of function value. (Contributed by set.mm contributors,
22May1998.)

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

Theorem  fnimapr 5414 
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 5415 
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 5416* 
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 5417 
The value of a function. Version of funfv2 5416 using a boundvariable
hypotheses instead of distinct variable conditions. (Contributed by NM,
19Feb2006.)

⊢ F/_yA & ⊢ F/_yF ⇒ ⊢ (Fun F
→ (F ‘A) = ∪{y ∣ AFy}) 

Theorem  fvun 5418 
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 5419 
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 5420 
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 5421 
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 5422 
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 5423 
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 5424 
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 5425* 
Closed theorem form of fvopab4 5429. (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 5426* 
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 5427* 
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 5428* 
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 5429* 
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 5430* 
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 5431* 
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  eqfnfv2 5432* 
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  eqfnfv 5433* 
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  eqfnfv3 5434* 
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 5435* 
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 5436* 
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 5433 uses boundvariable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29Jan2004.)

⊢ F/_xF & ⊢ F/_xG ⇒ ⊢ ((F Fn
A ∧
G Fn A) → (F =
G ↔ ∀x ∈ A (F ‘x) =
(G ‘x))) 

Theorem  eqfunfv 5437* 
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 5438* 
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 5439* 
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 5440 
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) 

Theorem  funfvbrb 5441 
Two ways to say that A is in
the domain of F.
(Contributed by
Mario Carneiro, 1May2014.)

⊢ (Fun F
→ (A ∈ dom F ↔
AF(F
‘A))) 

Theorem  fvimacnvi 5442 
A member of a preimage is a function value argument. (Contributed by
set.mm contributors, 4May2007.)

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

Theorem  fvimacnv 5443 
The argument of a function value belongs to the preimage of any class
containing the function value. (Contributed by Raph Levien, 20Nov2006.
He remarks: "This proof is unsatisfying, because it seems to me that
funimass2 5206 could probably be strengthened to a
biconditional.")
(Contributed by set.mm contributors, 20Nov2006.)

⊢ ((Fun F
∧ A ∈ dom F)
→ ((F ‘A) ∈ B ↔ A
∈ (^{◡}F
“ B))) 

Theorem  funimass3 5444 
A kind of contraposition law that infers an image subclass from a
subclass of a preimage. (Contributed by Raph Levien, 20Nov2006. He
remarks: "Likely this could be proved directly, and fvimacnv 5443 would be
the special case of A
being a singleton, but it works this way round
too.") (Contributed by set.mm contributors, 20Nov2006.)

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

Theorem  funimass5 5445* 
A subclass of a preimage in terms of function values. (Contributed by
set.mm contributors, 15May2007.)

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

Theorem  funconstss 5446* 
Two ways of specifying that a function is constant on a subdomain.
(Contributed by set.mm contributors, 8Mar2007.)

⊢ ((Fun F
∧ A ⊆ dom F)
→ (∀x ∈ A (F
‘x) = B ↔ A
⊆ (^{◡}F
“ {B}))) 

Theorem  elpreima 5447 
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2Sep2009.)

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

Theorem  unpreima 5448 
Preimage of a union. (Contributed by Jeff Madsen, 2Sep2009.)

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

Theorem  inpreima 5449 
Preimage of an intersection. (Contributed by Jeff Madsen,
2Sep2009.)

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

Theorem  respreima 5450 
The preimage of a restricted function. (Contributed by Jeff Madsen,
2Sep2009.)

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

Theorem  fimacnv 5451 
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25Jan2007.)

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

Theorem  fnopfv 5452 
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by set.mm contributors, 30Sep2004.)

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

Theorem  fvelrn 5453 
A function's value belongs to its range. (Contributed by set.mm
contributors, 14Oct1996.)

⊢ ((Fun F
∧ A ∈ dom F)
→ (F ‘A) ∈ ran F) 

Theorem  fnfvelrn 5454 
A function's value belongs to its range. (Contributed by set.mm
contributors, 15Oct1996.)

⊢ ((F Fn
A ∧
B ∈
A) → (F ‘B)
∈ ran F) 

Theorem  ffvelrn 5455 
A function's value belongs to its codomain. (Contributed by set.mm
contributors, 12Aug1999.)

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

Theorem  ffvelrni 5456 
A function's value belongs to its codomain. (Contributed by set.mm
contributors, 6Apr2005.)

⊢ F:A–→B ⇒ ⊢ (C ∈ A →
(F ‘C) ∈ B) 

Theorem  fnasrn 5457* 
A function expressed as the range of another function. (Contributed by
Mario Carneiro, 22Jun2013.)

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

Theorem  f0cli 5458 
Unconditional closure of a function when the range includes the empty
set. (Contributed by Mario Carneiro, 12Sep2013.)

⊢ F:A–→B
& ⊢ ∅ ∈ B ⇒ ⊢ (F
‘C) ∈ B 

Theorem  dff2 5459 
Alternate definition of a mapping. (Contributed by set.mm contributors,
14Nov2007.)

⊢ (F:A–→B
↔ (F Fn A ∧ F ⊆ (A × B))) 

Theorem  dff3 5460* 
Alternate definition of a mapping. (Contributed by set.mm contributors,
20Mar2007.)

⊢ (F:A–→B
↔ (F ⊆ (A ×
B) ∧
∀x
∈ A
∃!y
xFy)) 

Theorem  dff4 5461* 
Alternate definition of a mapping. (Contributed by set.mm contributors,
20Mar2007.)

⊢ (F:A–→B
↔ (F ⊆ (A ×
B) ∧
∀x
∈ A
∃!y
∈ B
xFy)) 

Theorem  dffo3 5462* 
An onto mapping expressed in terms of function values. (Contributed by
set.mm contributors, 29Oct2006.)

⊢ (F:A–onto→B ↔
(F:A–→B
∧ ∀y ∈ B ∃x ∈ A y = (F
‘x))) 

Theorem  dffo4 5463* 
Alternate definition of an onto mapping. (Contributed by set.mm
contributors, 20Mar2007.)

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

Theorem  dffo5 5464* 
Alternate definition of an onto mapping. (Contributed by set.mm
contributors, 20Mar2007.)

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

Theorem  foelrn 5465* 
Property of a surjective function. (Contributed by Jeff Madsen,
4Jan2011.)

⊢ ((F:A–onto→B
∧ C ∈ B) →
∃x
∈ A
C = (F
‘x)) 

Theorem  foco2 5466 
If a composition of two functions is surjective, then the function on
the left is surjective. (Contributed by Jeff Madsen, 16Jun2011.)

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

Theorem  ffnfv 5467* 
A function maps to a class to which all values belong. (Contributed by
NM, 3Dec2003.)

⊢ (F:A–→B
↔ (F Fn A ∧ ∀x ∈ A (F ‘x)
∈ B)) 

Theorem  ffnfvf 5468 
A function maps to a class to which all values belong. This version of
ffnfv 5467 uses boundvariable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28Sep2006.)

⊢ F/_xA & ⊢ F/_xB & ⊢ F/_xF ⇒ ⊢ (F:A–→B
↔ (F Fn A ∧ ∀x ∈ A (F ‘x)
∈ B)) 

Theorem  fnfvrnss 5469* 
An upper bound for range determined by function values. (Contributed by
set.mm contributors, 8Oct2004.)

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

Theorem  fopabfv 5470* 
Representation of a mapping in terms of its values. (Contributed by
set.mm contributors, 21Feb2004.)

⊢ (F:A–→B
↔ (F = {⟨x, y⟩ ∣ (x ∈ A ∧ y = (F ‘x))}
∧ ∀x ∈ A (F ‘x)
∈ B)) 

Theorem  ffvresb 5471* 
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14Nov2013.)

⊢ (Fun F
→ ((F ↾ A):A–→B
↔ ∀x ∈ A (x ∈ dom F ∧ (F
‘x) ∈ B))) 

Theorem  fsn 5472 
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 10Dec2003.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (F:{A}–→{B} ↔ F =
{⟨A,
B⟩}) 

Theorem  fsng 5473 
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by set.mm contributors, 26Oct2012.)

⊢ ((A ∈ C ∧ B ∈ D) →
(F:{A}–→{B} ↔ F =
{⟨A,
B⟩})) 

Theorem  fsn2 5474 
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by set.mm contributors, 19May2004.)

⊢ A ∈ V ⇒ ⊢ (F:{A}–→B ↔ ((F
‘A) ∈ B ∧ F = {⟨A, (F ‘A)⟩})) 

Theorem  xpsn 5475 
The cross product of two singletons. (Contributed by set.mm
contributors, 4Nov2006.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ({A}
× {B}) = {⟨A, B⟩} 

Theorem  ressnop0 5476 
If A is not in C, then the restriction of a
singleton of
⟨A, B⟩ to C is null. (Contributed by Scott Fenton,
15Apr2011.)

⊢ (¬ A
∈ C
→ ({⟨A, B⟩} ↾ C) = ∅) 

Theorem  fpr 5477 
A function with a domain of two elements. (Contributed by Jeff Madsen,
20Jun2010.) (The proof was shortened by Andrew Salmon,
22Oct2011.)

⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V ⇒ ⊢ (A ≠
B → {⟨A, C⟩, ⟨B, D⟩}:{A, B}–→{C, D}) 

Theorem  fnressn 5478 
A function restricted to a singleton. (Contributed by set.mm
contributors, 9Oct2004.)

⊢ ((F Fn
A ∧
B ∈
A) → (F ↾ {B}) = {⟨B, (F
‘B)⟩}) 

Theorem  fressnfv 5479 
The value of a function restricted to a singleton. (Contributed by
set.mm contributors, 9Oct2004.)

⊢ ((F Fn
A ∧
B ∈
A) → ((F ↾ {B}):{B}–→C ↔ (F
‘B) ∈ C)) 

Theorem  fvconst 5480 
The value of a constant function. (Contributed by set.mm contributors,
30May1999.)

⊢ ((F:A–→{B} ∧ C ∈ A) → (F
‘C) = B) 

Theorem  fopabsn 5481* 
The singleton of an ordered pair expressed as an ordered pair class
abstraction. (The proof was shortened by Andrew Salmon, 22Oct2011.)
(Contributed by set.mm contributors, 6Jun2006.) (Revised by set.mm
contributors, 22Oct2011.)

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

Theorem  fvi 5482 
The value of the identity function. (Contributed by set.mm
contributors, 1May2004.)

⊢ (A ∈ V → ( I
‘A) = A) 

Theorem  fvresi 5483 
The value of a restricted identity function. (Contributed by set.mm
contributors, 19May2004.)

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

Theorem  fvunsn 5484 
Remove an ordered pair not participating in a function value. (Revised by
Mario Carneiro, 28May2014.) (Contributed by set.mm contributors,
1Oct2013.) (Revised by set.mm contributors, 28May2014.)

⊢ (B ≠
D → ((A ∪ {⟨B, C⟩})
‘D) = (A ‘D)) 

Theorem  fvsn 5485 
The value of a singleton of an ordered pair is the second member.
(Contributed by set.mm contributors, 12Aug1994.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ({⟨A, B⟩} ‘A) =
B 

Theorem  fvsng 5486 
The value of a singleton of an ordered pair is the second member.
(Contributed by set.mm contributors, 26Oct2012.)

⊢ ((A ∈ V ∧ B ∈ W) →
({⟨A,
B⟩}
‘A) = B) 

Theorem  fvsnun1 5487 
The value of a function with one of its ordered pairs replaced, at the
replaced ordered pair. See also fvsnun2 5488. (Contributed by set.mm
contributors, 23Sep2007.)

⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ G = ({⟨A, B⟩} ∪
(F ↾
(C ∖
{A}))) ⇒ ⊢ (G
‘A) = B 

Theorem  fvsnun2 5488 
The value of a function with one of its ordered pairs replaced, at
arguments other than the replaced one. See also fvsnun1 5487.
(Contributed by set.mm contributors, 23Sep2007.)

⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ G = ({⟨A, B⟩} ∪
(F ↾
(C ∖
{A}))) ⇒ ⊢ (D ∈ (C ∖ {A}) →
(G ‘D) = (F
‘D)) 

Theorem  fvpr1 5489 
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20Jun2010.)

⊢ A ∈ V
& ⊢ C ∈ V ⇒ ⊢ (A ≠
B → ({⟨A, C⟩, ⟨B, D⟩}
‘A) = C) 

Theorem  fvpr2 5490 
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20Jun2010.)

⊢ B ∈ V
& ⊢ D ∈ V ⇒ ⊢ (A ≠
B → ({⟨A, C⟩, ⟨B, D⟩}
‘B) = D) 

Theorem  fvconst2g 5491 
The value of a constant function. (Contributed by set.mm contributors,
20Aug2005.)

⊢ ((B ∈ D ∧ C ∈ A) →
((A × {B}) ‘C) =
B) 

Theorem  fconst2g 5492 
A constant function expressed as a cross product. (Contributed by
set.mm contributors, 27Nov2007.)

⊢ (B ∈ C →
(F:A–→{B} ↔ F =
(A × {B}))) 

Theorem  fvconst2 5493 
The value of a constant function. (Contributed by set.mm contributors,
16Apr2005.)

⊢ B ∈ V ⇒ ⊢ (C ∈ A →
((A × {B}) ‘C) =
B) 

Theorem  fconst2 5494 
A constant function expressed as a cross product. (Contributed by
set.mm contributors, 20Aug1999.)

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

Theorem  fconst5 5495 
Two ways to express that a function is constant. (Contributed by set.mm
contributors, 27Nov2007.)

⊢ ((F Fn
A ∧
A ≠ ∅) → (F
= (A × {B}) ↔ ran F = {B})) 

Theorem  fconstfv 5496* 
A constant function expressed in terms of its functionality, domain, and
value. See also fconst2 5494. (Contributed by NM, 27Aug2004.)

⊢ (F:A–→{B} ↔ (F Fn
A ∧ ∀x ∈ A (F ‘x) =
B)) 

Theorem  fconst3 5497 
Two ways to express a constant function. (Contributed by set.mm
contributors, 15Mar2007.)

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

Theorem  fconst4 5498 
Two ways to express a constant function. (Contributed by set.mm
contributors, 8Mar2007.)

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

Theorem  funfvima 5499 
A function's value in a preimage belongs to the image. (Contributed by
set.mm contributors, 23Sep2003.)

⊢ ((Fun F
∧ B ∈ dom F)
→ (B ∈ A →
(F ‘B) ∈ (F “ A))) 

Theorem  funfvima2 5500 
A function's value in an included preimage belongs to the image.
(Contributed by set.mm contributors, 3Feb1997.)

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