Type  Label  Description 
Statement 

Theorem  cnvexg 5101 
The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring]
p. 26. (Contributed by set.mm contributors, 17Mar1998.)

⊢ (A ∈ V →
^{◡}A
∈ V) 

Theorem  cnvex 5102 
The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring]
p. 26. (Contributed by set.mm contributors, 19Dec2003.)

⊢ A ∈ V ⇒ ⊢ ^{◡}A ∈ V 

Theorem  cnvexb 5103 
A class is a set iff its converse is a set. (Contributed by FL,
3Mar2007.) (Revised by Scott Fenton, 18Apr2021.)

⊢ (R ∈ V ↔ ^{◡}R ∈ V) 

Theorem  rnexg 5104 
The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26.
Similar to Lemma 3D of [Enderton] p. 41.
(Contributed by set.mm
contributors, 8Jan2015.)

⊢ (A ∈ V → ran
A ∈
V) 

Theorem  dmexg 5105 
The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26.
(Contributed by set.mm contributors, 8Jan2015.)

⊢ (A ∈ V → dom
A ∈
V) 

Theorem  dmex 5106 
The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring]
p. 26. (Contributed by set.mm contributors, 7Jul2008.)

⊢ A ∈ V ⇒ ⊢ dom A ∈ V 

Theorem  rnex 5107 
The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26.
Similar to Lemma 3D of [Enderton] p.
41. (Contributed by set.mm
contributors, 7Jul2008.)

⊢ A ∈ V ⇒ ⊢ ran A ∈ V 

Theorem  elxp4 5108 
Membership in a cross product. This version requires no quantifiers or
dummy variables. (Contributed by set.mm contributors, 17Feb2004.)

⊢ (A ∈ (B ×
C) ↔ (A = ⟨∪dom {A}, ∪ran {A}⟩ ∧ (∪dom {A} ∈ B ∧ ∪ran {A} ∈ C))) 

Theorem  xpexr 5109 
If a cross product is a set, one of its components must be a set.
(Contributed by set.mm contributors, 27Aug2006.)

⊢ ((A ×
B) ∈
C → (A ∈ V ∨ B ∈ V)) 

Theorem  xpexr2 5110 
If a nonempty cross product is a set, so are both of its components.
(Contributed by set.mm contributors, 27Aug2006.) (Revised by set.mm
contributors, 5May2007.)

⊢ (((A
× B) ∈ C ∧ (A ×
B) ≠ ∅) → (A
∈ V ∧
B ∈
V)) 

Theorem  df2nd2 5111 
Alternate definition of the 2^{nd} function.
(Contributed by SF,
8Jan2015.)

⊢ 2^{nd} = (1^{st} ∘ Swap
) 

Theorem  2ndex 5112 
The 2^{nd} function is a set. (Contributed by SF,
8Jan2015.)

⊢ 2^{nd} ∈ V 

Theorem  dfxp2 5113 
Define cross product via the set construction functions. (Contributed
by SF, 8Jan2015.)

⊢ (A ×
B) = ((^{◡}1^{st} “ A) ∩ (^{◡}2^{nd} “ B)) 

Theorem  xpexg 5114 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. (Contributed
by set.mm contributors,
14Aug1994.)

⊢ ((A ∈ V ∧ B ∈ W) →
(A × B) ∈
V) 

Theorem  xpex 5115 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23.
(Contributed by set.mm contributors,
14Aug1994.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A ×
B) ∈
V 

Theorem  resexg 5116 
The restriction of a set to a set is a set. (Contributed by set.mm
contributors, 8Jan2015.)

⊢ ((A ∈ V ∧ B ∈ W) →
(A ↾
B) ∈
V) 

Theorem  resex 5117 
The restriction of a set to a set is a set. (Contributed by set.mm
contributors, 8Jan2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A ↾ B) ∈ V 

Theorem  cnviin 5118* 
The converse of an intersection is the intersection of the converse.
(Contributed by FL, 15Oct2012.) (Revised by Scott Fenton,
18Apr2021.)

⊢ ^{◡}∩x ∈ A B = ∩x ∈ A ^{◡}B 

Theorem  dffun2 5119* 
Alternate definition of a function. (Contributed by set.mm
contributors, 29Dec1996.) (Revised by set.mm contributors,
23Apr2004.) (Revised by Scott Fenton, 16Apr2021.)

⊢ (Fun A
↔ ∀x∀y∀z((xAy ∧ xAz) →
y = z)) 

Theorem  dffun3 5120* 
Alternate definition of function. (Contributed by NM, 29Dec1996.)
(Revised by Scott Fenton, 16Apr2021.)

⊢ (Fun A
↔ ∀x∃z∀y(xAy →
y = z)) 

Theorem  dffun4 5121* 
Alternate definition of a function. Definition 6.4(4) of
[TakeutiZaring] p. 24.
(Contributed by set.mm contributors,
29Dec1996.) (Revised by Scott Fenton, 16Apr2021.)

⊢ (Fun A
↔ ∀x∀y∀z((⟨x, y⟩ ∈ A ∧ ⟨x, z⟩ ∈ A) →
y = z)) 

Theorem  dffun5 5122* 
Alternate definition of function. (Contributed by set.mm contributors,
29Dec1996.) (Revised by Scott Fenton, 16Apr2021.)

⊢ (Fun A
↔ ∀x∃z∀y(⟨x, y⟩ ∈ A → y =
z)) 

Theorem  dffun6f 5123* 
Definition of function, using boundvariable hypotheses instead of
distinct variable conditions. (Contributed by NM, 9Mar1995.)
(Revised by Mario Carneiro, 15Oct2016.) (Revised by Scott Fenton,
16Apr2021.)

⊢ ℲxA & ⊢ ℲyA ⇒ ⊢ (Fun A
↔ ∀x∃*y xAy) 

Theorem  dffun6 5124* 
Alternate definition of a function using "at most one" notation.
(Contributed by NM, 9Mar1995.) (Revised by Scott Fenton,
16Apr2021.)

⊢ (Fun F
↔ ∀x∃*y xFy) 

Theorem  funmo 5125* 
A function has at most one value for each argument. (Contributed by NM,
24May1998.)

⊢ (Fun F
→ ∃*y AFy) 

Theorem  funss 5126 
Subclass theorem for function predicate. (The proof was shortened by
Mario Carneiro, 24Jun2014.) (Contributed by set.mm contributors,
16Aug1994.) (Revised by set.mm contributors, 24Jun2014.)

⊢ (A ⊆ B →
(Fun B → Fun A)) 

Theorem  funeq 5127 
Equality theorem for function predicate. (Contributed by set.mm
contributors, 16Aug1994.)

⊢ (A =
B → (Fun A ↔ Fun B)) 

Theorem  funeqi 5128 
Equality inference for the function predicate. (Contributed by Jonathan
BenNaim, 3Jun2011.)

⊢ A =
B ⇒ ⊢ (Fun A
↔ Fun B) 

Theorem  funeqd 5129 
Equality deduction for the function predicate. (Contributed by set.mm
contributors, 23Feb2013.)

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (Fun A ↔ Fun B)) 

Theorem  nffun 5130 
Boundvariable hypothesis builder for a function. (Contributed by NM,
30Jan2004.)

⊢ ℲxF ⇒ ⊢ ℲxFun
F 

Theorem  funeu 5131* 
There is exactly one value of a function. (Contributed by NM,
22Apr2004.) (Proof shortened by Andrew Salmon, 17Sep2011.)

⊢ ((Fun F
∧ AFB) → ∃!y AFy) 

Theorem  funeu2 5132* 
There is exactly one value of a function. (Contributed by NM,
3Aug1994.)

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

Theorem  dffun7 5133* 
Alternate definition of a function. One possibility for the definition
of a function in [Enderton] p. 42.
(Enderton's definition is ambiguous
because "there is only one" could mean either "there is
at most one" or
"there is exactly one." However, dffun8 5134 shows that it doesn't matter
which meaning we pick.) (Contributed by set.mm contributors,
4Nov2002.) (Revised by Scott Fenton, 16Apr2021.)

⊢ (Fun A
↔ ∀x ∈ dom A∃*y xAy) 

Theorem  dffun8 5134* 
Alternate definition of a function. One possibility for the definition
of a function in [Enderton] p. 42.
Compare dffun7 5133. (The proof was
shortened by Andrew Salmon, 17Sep2011.) (Contributed by set.mm
contributors, 4Nov2002.) (Revised by set.mm contributors,
18Sep2011.) (Revised by Scott Fenton, 16Apr2021.)

⊢ (Fun A
↔ ∀x ∈ dom A∃!y xAy) 

Theorem  dffun9 5135* 
Alternate definition of a function. (Contributed by set.mm
contributors, 28Mar2007.) (Revised by Scott Fenton, 16Apr2021.)

⊢ (Fun A
↔ ∀x ∈ dom A∃*y(y ∈ ran A ∧ xAy)) 

Theorem  funfn 5136 
An equivalence for the function predicate. (Contributed by set.mm
contributors, 13Aug2004.)

⊢ (Fun A
↔ A Fn dom A) 

Theorem  funi 5137 
The identity relation is a function. Part of Theorem 10.4 of [Quine]
p. 65. (Contributed by set.mm contributors, 30Apr1998.)

⊢ Fun I 

Theorem  nfunv 5138 
The universe is not a function. (Contributed by Raph Levien,
27Jan2004.)

⊢ ¬ Fun V 

Theorem  funopab 5139* 
A class of ordered pairs is a function when there is at most one second
member for each pair. (Contributed by NM, 16May1995.)

⊢ (Fun {⟨x, y⟩ ∣ φ}
↔ ∀x∃*yφ) 

Theorem  funopabeq 5140* 
A class of ordered pairs of values is a function. (Contributed by
set.mm contributors, 14Nov1995.)

⊢ Fun {⟨x, y⟩ ∣ y =
A} 

Theorem  funopab4 5141* 
A class of ordered pairs of values in the form used by fvopab4 5389 is a
function. (Contributed by set.mm contributors, 17Feb2013.)

⊢ Fun {⟨x, y⟩ ∣ (φ
∧ y =
A)} 

Theorem  funco 5142 
The composition of two functions is a function. Exercise 29 of
[TakeutiZaring] p. 25.
(Contributed by NM, 26Jan1997.) (Proof
shortened by Andrew Salmon, 17Sep2011.)

⊢ ((Fun F
∧ Fun G)
→ Fun (F ∘ G)) 

Theorem  funres 5143 
A restriction of a function is a function. Compare Exercise 18 of
[TakeutiZaring] p. 25. (Contributed
by set.mm contributors,
16Aug1994.)

⊢ (Fun F
→ Fun (F ↾ A)) 

Theorem  funssres 5144 
The restriction of a function to the domain of a subclass equals the
subclass. (Contributed by NM, 15Aug1994.)

⊢ ((Fun F
∧ G ⊆ F) →
(F ↾
dom G) = G) 

Theorem  fun2ssres 5145 
Equality of restrictions of a function and a subclass. (Contributed by
set.mm contributors, 16Aug1994.) (Revised by set.mm contributors,
2Jun2007.)

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

Theorem  funun 5146 
The union of functions with disjoint domains is a function. Theorem 4.6
of [Monk1] p. 43. (Contributed by set.mm
contributors, 12Aug1994.)

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

Theorem  funsn 5147 
A singleton of an ordered pair is a function. Theorem 10.5 of [Quine]
p. 65. (Contributed by NM, 12Aug1994.) (Revised by Scott Fenton,
16Apr2021.)

⊢ Fun {⟨A, B⟩} 

Theorem  funsngOLD 5148 
A singleton of an ordered pair is a function. Theorem 10.5 of [Quine]
p. 65. (Contributed by set.mm contributors, 28Jun2011.) (Revised by
set.mm contributors, 1Oct2013.) (Proof modification is discouraged.)
(New usage is discouraged.)

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

Theorem  funprg 5149 
A set of two pairs is a function if their first members are different.
(Contributed by FL, 26Jun2011.) (Revised by Scott Fenton,
16Apr2021.)

⊢ ((A ≠
B ∧
C ∈
V ∧
D ∈
W) → Fun {⟨A, C⟩, ⟨B, D⟩}) 

Theorem  funprgOLD 5150 
A set of two pairs is a function if their first members are different.
(Contributed by FL, 26Jun2011.) (Proof modification is discouraged.)
(New usage is discouraged.)

⊢ ((A ≠
B ∧
(A ∈
V ∧
B ∈
W) ∧
(C ∈
T ∧
D ∈
U)) → Fun {⟨A, C⟩, ⟨B, D⟩}) 

Theorem  funpr 5151 
A function with a domain of two elements. (Contributed by Jeff Madsen,
20Jun2010.)

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

Theorem  fnsn 5152 
Functionality and domain of the singleton of an ordered pair.
(Contributed by Jonathan BenNaim, 3Jun2011.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ {⟨A, B⟩} Fn {A} 

Theorem  fnprg 5153 
Domain of a function with a domain of two different values. (Contributed
by FL, 26Jun2011.)

⊢ ((A ≠
B ∧
(A ∈
V ∧
B ∈
W) ∧
(C ∈
T ∧
D ∈
U)) → {⟨A, C⟩, ⟨B, D⟩} Fn {A, B}) 

Theorem  fun0 5154 
The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed
by set.mm contributors, 7Apr1998.)

⊢ Fun ∅ 

Theorem  funcnv2 5155* 
A simpler equivalence for singlerooted (see funcnv 5156). (Contributed
by set.mm contributors, 9Aug2004.)

⊢ (Fun ^{◡}A
↔ ∀y∃*x xAy) 

Theorem  funcnv 5156* 
The converse of a class is a function iff the class is singlerooted,
which means that for any y in the range of A there is at most
one x such that xAy.
Definition of singlerooted in
[Enderton] p. 43. See funcnv2 5155 for a simpler version. (Contributed by
set.mm contributors, 13Aug2004.)

⊢ (Fun ^{◡}A
↔ ∀y ∈ ran A∃*x xAy) 

Theorem  funcnv3 5157* 
A condition showing a class is singlerooted. (See funcnv 5156).
(Contributed by set.mm contributors, 26May2006.)

⊢ (Fun ^{◡}A
↔ ∀y ∈ ran A∃!x ∈ dom A xAy) 

Theorem  fncnv 5158* 
Singlerootedness (see funcnv 5156) of a class cut down by a cross
product. (Contributed by NM, 5Mar2007.)

⊢ (^{◡}(R
∩ (A × B)) Fn B ↔
∀y
∈ B
∃!x
∈ A
xRy) 

Theorem  fun11 5159* 
Two ways of stating that 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.
(Contributed by NM, 17Jan2006.) (Revised
by Scott Fenton, 18Apr2021.)

⊢ ((Fun A
∧ Fun ^{◡}A)
↔ ∀x∀y∀z∀w((xAy ∧ zAw) →
(x = z
↔ y = w))) 

Theorem  fununi 5160* 
The union of a chain (with respect to inclusion) of functions is a
function. (Contributed by set.mm contributors, 10Aug2004.)

⊢ (∀f ∈ A (Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) →
Fun ∪A) 

Theorem  funcnvuni 5161* 
The union of a chain (with respect to inclusion) of singlerooted sets
is singlerooted. (See funcnv 5156 for "singlerooted"
definition.)
(Contributed by set.mm contributors, 11Aug2004.)

⊢ (∀f ∈ A (Fun ^{◡}f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) →
Fun ^{◡}∪A) 

Theorem  fun11uni 5162* 
The union of a chain (with respect to inclusion) of onetoone functions
is a onetoone function. (Contributed by set.mm contributors,
11Aug2004.)

⊢ (∀f ∈ A ((Fun f ∧ Fun ^{◡}f)
∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → (Fun ∪A ∧ Fun ^{◡}∪A)) 

Theorem  funin 5163 
The intersection with a function is a function. Exercise 14(a) of
[Enderton] p. 53. (The proof was
shortened by Andrew Salmon,
17Sep2011.) (Contributed by set.mm contributors, 19Mar2004.)
(Revised by set.mm contributors, 18Sep2011.)

⊢ (Fun F
→ Fun (F ∩ G)) 

Theorem  funres11 5164 
The restriction of a onetoone function is onetoone. (Contributed by
set.mm contributors, 25Mar1998.)

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

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

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

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

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

Theorem  funcnvres2 5167 
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 5168 
The image of the preimage of a function. (Contributed by set.mm
contributors, 25May2004.)

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

Theorem  funimass1 5169 
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 5170 
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 5171 
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 5172 
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 5173 
Equality theorem for function predicate with domain. (Contributed by
set.mm contributors, 1Aug1994.)

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

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

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

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

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

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

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

Theorem  fneq12d 5177 
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 5178 
Equality inference for function predicate with domain. (Contributed by
Paul Chapman, 22Jun2011.)

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

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

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

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

⊢ ℲxF & ⊢ ℲxA ⇒ ⊢ Ⅎx
F Fn A 

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

⊢ (F Fn
A → Fun F) 

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

⊢ (F Fn
A → dom F = A) 

Theorem  funfni 5183 
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 5184 
A function has a unique domain. (Contributed by set.mm contributors,
11Aug1994.)

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

Theorem  fnbr 5185 
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 5186 
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 5187* 
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 5188* 
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 5189 
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 5190 
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 5191 
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 5192 
A function does not change when restricted to its domain. (Contributed by
set.mm contributors, 5Sep2004.)

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

Theorem  fnresdisj 5193 
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 5194 
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 5195 
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 5196 
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 5197 
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 5198 
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 5199* 
An equivalence for functionality of a restriction. Compare dffun8 5134.
(Contributed by Mario Carneiro, 20May2015.)

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

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

⊢ ( I ↾
A) Fn A 