P. 52 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5101-5200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfcnv2 5101	Definition of converse in terms of image and Swap . (Contributed by set.mm contributors, 8-Jan-2015.)
⊢ ◡A = ( Swap “ A)
Theorem	cnvexg 5102	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by set.mm contributors, 17-Mar-1998.)
⊢ (A ∈ V → ◡A ∈ V)
Theorem	cnvex 5103	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by set.mm contributors, 19-Dec-2003.)
⊢ A ∈ V    ⇒   ⊢ ◡A ∈ V
Theorem	cnvexb 5104	A class is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.) (Revised by Scott Fenton, 18-Apr-2021.)
⊢ (R ∈ V ↔ ◡R ∈ V)
Theorem	rnexg 5105	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, 8-Jan-2015.)
⊢ (A ∈ V → ran A ∈ V)
Theorem	dmexg 5106	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by set.mm contributors, 8-Jan-2015.)
⊢ (A ∈ V → dom A ∈ V)
Theorem	dmex 5107	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by set.mm contributors, 7-Jul-2008.)
⊢ A ∈ V    ⇒   ⊢ dom A ∈ V
Theorem	rnex 5108	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, 7-Jul-2008.)
⊢ A ∈ V    ⇒   ⊢ ran A ∈ V
Theorem	elxp4 5109	Membership in a cross product. This version requires no quantifiers or dummy variables. (Contributed by set.mm contributors, 17-Feb-2004.)
⊢ (A ∈ (B × C) ↔ (A = ⟨∪dom {A}, ∪ran {A}⟩ ∧ (∪dom {A} ∈ B ∧ ∪ran {A} ∈ C)))
Theorem	xpexr 5110	If a cross product is a set, one of its components must be a set. (Contributed by set.mm contributors, 27-Aug-2006.)
⊢ ((A × B) ∈ C → (A ∈ V ∨ B ∈ V))
Theorem	xpexr2 5111	If a nonempty cross product is a set, so are both of its components. (Contributed by set.mm contributors, 27-Aug-2006.) (Revised by set.mm contributors, 5-May-2007.)
⊢ (((A × B) ∈ C ∧ (A × B) ≠ ∅) → (A ∈ V ∧ B ∈ V))
Theorem	df2nd2 5112	Alternate definition of the 2nd function. (Contributed by SF, 8-Jan-2015.)
⊢ 2nd = (1st ∘ Swap )
Theorem	2ndex 5113	The 2nd function is a set. (Contributed by SF, 8-Jan-2015.)
⊢ 2nd ∈ V
Theorem	dfxp2 5114	Define cross product via the set construction functions. (Contributed by SF, 8-Jan-2015.)
⊢ (A × B) = ((◡1st “ A) ∩ (◡2nd “ B))
Theorem	xpexg 5115	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by set.mm contributors, 14-Aug-1994.)
⊢ ((A ∈ V ∧ B ∈ W) → (A × B) ∈ V)
Theorem	xpex 5116	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by set.mm contributors, 14-Aug-1994.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A × B) ∈ V
Theorem	resexg 5117	The restriction of a set to a set is a set. (Contributed by set.mm contributors, 8-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A ↾ B) ∈ V)
Theorem	resex 5118	The restriction of a set to a set is a set. (Contributed by set.mm contributors, 8-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ↾ B) ∈ V
Theorem	cnviin 5119*	The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012.) (Revised by Scott Fenton, 18-Apr-2021.)
⊢ ◡∩x ∈ A B = ∩x ∈ A ◡B
Theorem	dffun2 5120*	Alternate definition of a function. (Contributed by set.mm contributors, 29-Dec-1996.) (Revised by set.mm contributors, 23-Apr-2004.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (Fun A ↔ ∀x∀y∀z((xAy ∧ xAz) → y = z))
Theorem	dffun3 5121*	Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (Fun A ↔ ∀x∃z∀y(xAy → y = z))
Theorem	dffun4 5122*	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by set.mm contributors, 29-Dec-1996.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (Fun A ↔ ∀x∀y∀z((⟨x, y⟩ ∈ A ∧ ⟨x, z⟩ ∈ A) → y = z))
Theorem	dffun5 5123*	Alternate definition of function. (Contributed by set.mm contributors, 29-Dec-1996.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (Fun A ↔ ∀x∃z∀y(⟨x, y⟩ ∈ A → y = z))
Theorem	dffun6f 5124*	Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ ℲxA    &   ⊢ ℲyA    ⇒   ⊢ (Fun A ↔ ∀x∃*y xAy)
Theorem	dffun6 5125*	Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (Fun F ↔ ∀x∃*y xFy)
Theorem	funmo 5126*	A function has at most one value for each argument. (Contributed by NM, 24-May-1998.)
⊢ (Fun F → ∃*y AFy)
Theorem	funss 5127	Subclass theorem for function predicate. (The proof was shortened by Mario Carneiro, 24-Jun-2014.) (Contributed by set.mm contributors, 16-Aug-1994.) (Revised by set.mm contributors, 24-Jun-2014.)
⊢ (A ⊆ B → (Fun B → Fun A))
Theorem	funeq 5128	Equality theorem for function predicate. (Contributed by set.mm contributors, 16-Aug-1994.)
⊢ (A = B → (Fun A ↔ Fun B))
Theorem	funeqi 5129	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ A = B    ⇒   ⊢ (Fun A ↔ Fun B)
Theorem	funeqd 5130	Equality deduction for the function predicate. (Contributed by set.mm contributors, 23-Feb-2013.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (Fun A ↔ Fun B))
Theorem	nffun 5131	Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
⊢ ℲxF    ⇒   ⊢ ℲxFun F
Theorem	funeu 5132*	There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((Fun F ∧ AFB) → ∃!y AFy)
Theorem	funeu2 5133*	There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.)
⊢ ((Fun F ∧ ⟨A, B⟩ ∈ F) → ∃!y⟨A, y⟩ ∈ F)
Theorem	dffun7 5134*	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 5135 shows that it doesn't matter which meaning we pick.) (Contributed by set.mm contributors, 4-Nov-2002.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (Fun A ↔ ∀x ∈ dom A∃*y xAy)
Theorem	dffun8 5135*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 5134. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 4-Nov-2002.) (Revised by set.mm contributors, 18-Sep-2011.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (Fun A ↔ ∀x ∈ dom A∃!y xAy)
Theorem	dffun9 5136*	Alternate definition of a function. (Contributed by set.mm contributors, 28-Mar-2007.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ (Fun A ↔ ∀x ∈ dom A∃*y(y ∈ ran A ∧ xAy))
Theorem	funfn 5137	An equivalence for the function predicate. (Contributed by set.mm contributors, 13-Aug-2004.)
⊢ (Fun A ↔ A Fn dom A)
Theorem	funi 5138	The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. (Contributed by set.mm contributors, 30-Apr-1998.)
⊢ Fun I
Theorem	nfunv 5139	The universe is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
⊢ ¬ Fun V
Theorem	funopab 5140*	A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995.)
⊢ (Fun {⟨x, y⟩ ∣ φ} ↔ ∀x∃*yφ)
Theorem	funopabeq 5141*	A class of ordered pairs of values is a function. (Contributed by set.mm contributors, 14-Nov-1995.)
⊢ Fun {⟨x, y⟩ ∣ y = A}
Theorem	funopab4 5142*	A class of ordered pairs of values in the form used by fvopab4 5390 is a function. (Contributed by set.mm contributors, 17-Feb-2013.)
⊢ Fun {⟨x, y⟩ ∣ (φ ∧ y = A)}
Theorem	funco 5143	The composition of two functions is a function. Exercise 29 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((Fun F ∧ Fun G) → Fun (F ∘ G))
Theorem	funres 5144	A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 16-Aug-1994.)
⊢ (Fun F → Fun (F ↾ A))
Theorem	funssres 5145	The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.)
⊢ ((Fun F ∧ G ⊆ F) → (F ↾ dom G) = G)
Theorem	fun2ssres 5146	Equality of restrictions of a function and a subclass. (Contributed by set.mm contributors, 16-Aug-1994.) (Revised by set.mm contributors, 2-Jun-2007.)
⊢ ((Fun F ∧ G ⊆ F ∧ A ⊆ dom G) → (F ↾ A) = (G ↾ A))
Theorem	funun 5147	The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by set.mm contributors, 12-Aug-1994.)
⊢ (((Fun F ∧ Fun G) ∧ (dom F ∩ dom G) = ∅) → Fun (F ∪ G))
Theorem	funsn 5148	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 12-Aug-1994.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ Fun {⟨A, B⟩}
Theorem	funsngOLD 5149	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by set.mm contributors, 28-Jun-2011.) (Revised by set.mm contributors, 1-Oct-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((A ∈ V ∧ B ∈ W) → Fun {⟨A, B⟩})
Theorem	funprg 5150	A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.) (Revised by Scott Fenton, 16-Apr-2021.)
⊢ ((A ≠ B ∧ C ∈ V ∧ D ∈ W) → Fun {⟨A, C⟩, ⟨B, D⟩})
Theorem	funprgOLD 5151	A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.) (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 5152	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
⊢ C ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ (A ≠ B → Fun {⟨A, C⟩, ⟨B, D⟩})
Theorem	fnsn 5153	Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ {⟨A, B⟩} Fn {A}
Theorem	fnprg 5154	Domain of a function with a domain of two different values. (Contributed by FL, 26-Jun-2011.)
⊢ ((A ≠ B ∧ (A ∈ V ∧ B ∈ W) ∧ (C ∈ T ∧ D ∈ U)) → {⟨A, C⟩, ⟨B, D⟩} Fn {A, B})
Theorem	fun0 5155	The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by set.mm contributors, 7-Apr-1998.)
⊢ Fun ∅
Theorem	funcnv2 5156*	A simpler equivalence for single-rooted (see funcnv 5157). (Contributed by set.mm contributors, 9-Aug-2004.)
⊢ (Fun ◡A ↔ ∀y∃*x xAy)
Theorem	funcnv 5157*	The converse of a class is a function iff the class is single-rooted, which means that for any y in the range of A there is at most one x such that xAy. Definition of single-rooted in [Enderton] p. 43. See funcnv2 5156 for a simpler version. (Contributed by set.mm contributors, 13-Aug-2004.)
⊢ (Fun ◡A ↔ ∀y ∈ ran A∃*x xAy)
Theorem	funcnv3 5158*	A condition showing a class is single-rooted. (See funcnv 5157). (Contributed by set.mm contributors, 26-May-2006.)
⊢ (Fun ◡A ↔ ∀y ∈ ran A∃!x ∈ dom A xAy)
Theorem	fncnv 5159*	Single-rootedness (see funcnv 5157) of a class cut down by a cross product. (Contributed by NM, 5-Mar-2007.)
⊢ (◡(R ∩ (A × B)) Fn B ↔ ∀y ∈ B ∃!x ∈ A xRy)
Theorem	fun11 5160*	Two ways of stating that A is one-to-one. Each side is equivalent to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation "Un2 (A)" for one-to-one. (Contributed by NM, 17-Jan-2006.) (Revised by Scott Fenton, 18-Apr-2021.)
⊢ ((Fun A ∧ Fun ◡A) ↔ ∀x∀y∀z∀w((xAy ∧ zAw) → (x = z ↔ y = w)))
Theorem	fununi 5161*	The union of a chain (with respect to inclusion) of functions is a function. (Contributed by set.mm contributors, 10-Aug-2004.)
⊢ (∀f ∈ A (Fun f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → Fun ∪A)
Theorem	funcnvuni 5162*	The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 5157 for "single-rooted" definition.) (Contributed by set.mm contributors, 11-Aug-2004.)
⊢ (∀f ∈ A (Fun ◡f ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → Fun ◡∪A)
Theorem	fun11uni 5163*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by set.mm contributors, 11-Aug-2004.)
⊢ (∀f ∈ A ((Fun f ∧ Fun ◡f) ∧ ∀g ∈ A (f ⊆ g ∨ g ⊆ f)) → (Fun ∪A ∧ Fun ◡∪A))
Theorem	funin 5164	The intersection with a function is a function. Exercise 14(a) of [Enderton] p. 53. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 19-Mar-2004.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ (Fun F → Fun (F ∩ G))
Theorem	funres11 5165	The restriction of a one-to-one function is one-to-one. (Contributed by set.mm contributors, 25-Mar-1998.)
⊢ (Fun ◡F → Fun ◡(F ↾ A))
Theorem	funcnvres 5166	The converse of a restricted function. (Contributed by set.mm contributors, 27-Mar-1998.)
⊢ (Fun ◡F → ◡(F ↾ A) = (◡F ↾ (F “ A)))
Theorem	cnvresid 5167	Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.)
⊢ ◡( I ↾ A) = ( I ↾ A)
Theorem	funcnvres2 5168	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, 4-May-2005.)
⊢ (Fun F → ◡(◡F ↾ A) = (F ↾ (◡F “ A)))
Theorem	funimacnv 5169	The image of the preimage of a function. (Contributed by set.mm contributors, 25-May-2004.)
⊢ (Fun F → (F “ (◡F “ A)) = (A ∩ ran F))
Theorem	funimass1 5170	A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by set.mm contributors, 25-May-2004.)
⊢ ((Fun F ∧ A ⊆ ran F) → ((◡F “ A) ⊆ B → A ⊆ (F “ B)))
Theorem	funimass2 5171	A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by set.mm contributors, 25-May-2004.) (Revised by set.mm contributors, 4-May-2007.)
⊢ ((Fun F ∧ A ⊆ (◡F “ B)) → (F “ A) ⊆ B)
Theorem	imadif 5172	The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)
⊢ (Fun ◡F → (F “ (A ∖ B)) = ((F “ A) ∖ (F “ B)))
Theorem	imain 5173	The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ (Fun ◡F → (F “ (A ∩ B)) = ((F “ A) ∩ (F “ B)))
Theorem	fneq1 5174	Equality theorem for function predicate with domain. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (F = G → (F Fn A ↔ G Fn A))
Theorem	fneq2 5175	Equality theorem for function predicate with domain. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (A = B → (F Fn A ↔ F Fn B))
Theorem	fneq1d 5176	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (φ → F = G)    ⇒   ⊢ (φ → (F Fn A ↔ G Fn A))
Theorem	fneq2d 5177	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (F Fn A ↔ F Fn B))
Theorem	fneq12d 5178	Equality deduction for function predicate with domain. (Contributed by set.mm contributors, 26-Jun-2011.)
⊢ (φ → F = G)    &   ⊢ (φ → A = B)    ⇒   ⊢ (φ → (F Fn A ↔ G Fn B))
Theorem	fneq1i 5179	Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ F = G    ⇒   ⊢ (F Fn A ↔ G Fn A)
Theorem	fneq2i 5180	Equality inference for function predicate with domain. (Contributed by set.mm contributors, 4-Sep-2011.)
⊢ A = B    ⇒   ⊢ (F Fn A ↔ F Fn B)
Theorem	nffn 5181	Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)
⊢ ℲxF    &   ⊢ ℲxA    ⇒   ⊢ Ⅎx F Fn A
Theorem	fnfun 5182	A function with domain is a function. (Contributed by set.mm contributors, 1-Aug-1994.)
⊢ (F Fn A → Fun F)
Theorem	fndm 5183	The domain of a function. (Contributed by set.mm contributors, 2-Aug-1994.)
⊢ (F Fn A → dom F = A)
Theorem	funfni 5184	Inference to convert a function and domain antecedent. (Contributed by set.mm contributors, 22-Apr-2004.)
⊢ ((Fun F ∧ B ∈ dom F) → φ)    ⇒   ⊢ ((F Fn A ∧ B ∈ A) → φ)
Theorem	fndmu 5185	A function has a unique domain. (Contributed by set.mm contributors, 11-Aug-1994.)
⊢ ((F Fn A ∧ F Fn B) → A = B)
Theorem	fnbr 5186	The first argument of binary relation on a function belongs to the function's domain. (Contributed by set.mm contributors, 7-May-2004.)
⊢ ((F Fn A ∧ BFC) → B ∈ A)
Theorem	fnop 5187	The first argument of an ordered pair in a function belongs to the function's domain. (Contributed by set.mm contributors, 8-Aug-1994.) (Revised by set.mm contributors, 25-Mar-2007.)
⊢ ((F Fn A ∧ ⟨B, C⟩ ∈ F) → B ∈ A)
Theorem	fneu 5188*	There is exactly one value of a function. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 22-Apr-2004.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ ((F Fn A ∧ B ∈ A) → ∃!y BFy)
Theorem	fneu2 5189*	There is exactly one value of a function. (Contributed by set.mm contributors, 7-Nov-1995.)
⊢ ((F Fn A ∧ B ∈ A) → ∃!y⟨B, y⟩ ∈ F)
Theorem	fnun 5190	The union of two functions with disjoint domains. (Contributed by set.mm contributors, 22-Sep-2004.)
⊢ (((F Fn A ∧ G Fn B) ∧ (A ∩ B) = ∅) → (F ∪ G) Fn (A ∪ B))
Theorem	fnunsn 5191	Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013.)
⊢ (φ → X ∈ V)    &   ⊢ (φ → Y ∈ V)    &   ⊢ (φ → F Fn D)    &   ⊢ G = (F ∪ {⟨X, Y⟩})    &   ⊢ E = (D ∪ {X})    &   ⊢ (φ → ¬ X ∈ D)    ⇒   ⊢ (φ → G Fn E)
Theorem	fnco 5192	Composition of two functions. (Contributed by set.mm contributors, 22-May-2006.)
⊢ ((F Fn A ∧ G Fn B ∧ ran G ⊆ A) → (F ∘ G) Fn B)
Theorem	fnresdm 5193	A function does not change when restricted to its domain. (Contributed by set.mm contributors, 5-Sep-2004.)
⊢ (F Fn A → (F ↾ A) = F)
Theorem	fnresdisj 5194	A function restricted to a class disjoint with its domain is empty. (Contributed by set.mm contributors, 23-Sep-2004.)
⊢ (F Fn A → ((A ∩ B) = ∅ ↔ (F ↾ B) = ∅))
Theorem	2elresin 5195	Membership in two functions restricted by each other's domain. (Contributed by set.mm contributors, 8-Aug-1994.)
⊢ ((F Fn A ∧ G Fn B) → ((⟨x, y⟩ ∈ F ∧ ⟨x, z⟩ ∈ G) ↔ (⟨x, y⟩ ∈ (F ↾ (A ∩ B)) ∧ ⟨x, z⟩ ∈ (G ↾ (A ∩ B)))))
Theorem	fnssresb 5196	Restriction of a function with a subclass of its domain. (Contributed by set.mm contributors, 10-Oct-2007.)
⊢ (F Fn A → ((F ↾ B) Fn B ↔ B ⊆ A))
Theorem	fnssres 5197	Restriction of a function with a subclass of its domain. (Contributed by set.mm contributors, 2-Aug-1994.) (Revised by set.mm contributors, 25-Sep-2004.)
⊢ ((F Fn A ∧ B ⊆ A) → (F ↾ B) Fn B)
Theorem	fnresin1 5198	Restriction of a function's domain with an intersection. (Contributed by set.mm contributors, 9-Aug-1994.)
⊢ (F Fn A → (F ↾ (A ∩ B)) Fn (A ∩ B))
Theorem	fnresin2 5199	Restriction of a function's domain with an intersection. (Contributed by set.mm contributors, 9-Aug-1994.)
⊢ (F Fn A → (F ↾ (B ∩ A)) Fn (B ∩ A))
Theorem	fnres 5200*	An equivalence for functionality of a restriction. Compare dffun8 5135. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ ((F ↾ A) Fn A ↔ ∀x ∈ A ∃!y xFy)