P. 54 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5301-5400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	f1orescnv 5301	The converse of a one-to-one-onto restricted function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((Fun ◡F ∧ (F ↾ R):R–1-1-onto→P) → (◡F ↾ P):P–1-1-onto→R)
Theorem	f1imacnv 5302	Preimage of an image. (Contributed by set.mm contributors, 30-Sep-2004.)
⊢ ((F:A–1-1→B ∧ C ⊆ A) → (◡F “ (F “ C)) = C)
Theorem	foimacnv 5303	A reverse version of f1imacnv 5302. (Contributed by Jeffrey Hankins, 16-Jul-2009.)
⊢ ((F:A–onto→B ∧ C ⊆ B) → (F “ (◡F “ C)) = C)
Theorem	f1oun 5304	The union of two one-to-one onto functions with disjoint domains and ranges. (Contributed by set.mm contributors, 26-Mar-1998.)
⊢ (((F:A–1-1-onto→B ∧ G:C–1-1-onto→D) ∧ ((A ∩ C) = ∅ ∧ (B ∩ D) = ∅)) → (F ∪ G):(A ∪ C)–1-1-onto→(B ∪ D))
Theorem	fun11iun 5305*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ (x = y → B = C)    &   ⊢ B ∈ V    ⇒   ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) → ∪x ∈ A B:∪x ∈ A D–1-1→S)
Theorem	resdif 5306	The restriction of a one-to-one onto function to a difference maps onto the difference of the images. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ ((Fun ◡F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) → (F ↾ (A ∖ B)):(A ∖ B)–1-1-onto→(C ∖ D))
Theorem	resin 5307	The restriction of a one-to-one onto function to an intersection maps onto the intersection of the images. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ ((Fun ◡F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) → (F ↾ (A ∩ B)):(A ∩ B)–1-1-onto→(C ∩ D))
Theorem	f1oco 5308	Composition of one-to-one onto functions. (Contributed by set.mm contributors, 19-Mar-1998.)
⊢ ((F:B–1-1-onto→C ∧ G:A–1-1-onto→B) → (F ∘ G):A–1-1-onto→C)
Theorem	f1ococnv2 5309	The composition of a one-to-one onto function and its converse equals the identity relation restricted to the function's range. (Contributed by set.mm contributors, 13-Dec-2003.)
⊢ (F:A–1-1-onto→B → (F ∘ ◡F) = ( I ↾ B))
Theorem	f1ococnv1 5310	The composition of a one-to-one onto function's converse and itself equals the identity relation restricted to the function's domain. (Contributed by set.mm contributors, 13-Dec-2003.)
⊢ (F:A–1-1-onto→B → (◡F ∘ F) = ( I ↾ A))
Theorem	f1cnv 5311	The converse of an injective function is bijective. (Contributed by FL, 11-Nov-2011.)
⊢ (F:A–1-1→B → ◡F:ran F–1-1-onto→A)
Theorem	f1cocnv1 5312	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (F:A–1-1→B → (◡F ∘ F) = ( I ↾ A))
Theorem	f1cocnv2 5313	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (F:A–1-1→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, 10-May-1998.)
⊢ F ∈ V    ⇒   ⊢ (F:A–→B ↔ ∃x(F:A–onto→x ∧ x ⊆ B))
Theorem	f11o 5315*	Relationship between one-to-one and one-to-one onto function. (Contributed by set.mm contributors, 4-Apr-1998.)
⊢ F ∈ V    ⇒   ⊢ (F:A–1-1→B ↔ ∃x(F:A–1-1-onto→x ∧ x ⊆ B))
Theorem	f10 5316	The empty set maps one-to-one into any class. (Contributed by set.mm contributors, 7-Apr-1998.)
⊢ ∅:∅–1-1→A
Theorem	f1o00 5317	One-to-one onto mapping of the empty set. (Contributed by set.mm contributors, 15-Apr-1998.)
⊢ (F:∅–1-1-onto→A ↔ (F = ∅ ∧ A = ∅))
Theorem	fo00 5318	Onto mapping of the empty set. (Contributed by set.mm contributors, 22-Mar-2006.)
⊢ (F:∅–onto→A ↔ (F = ∅ ∧ A = ∅))
Theorem	f1o0 5319	One-to-one onto mapping of the empty set. (Contributed by set.mm contributors, 10-Feb-2004.) (Revised by set.mm contributors, 16-Feb-2004.)
⊢ ∅:∅–1-1-onto→∅
Theorem	f1oi 5320	A restriction of the identity relation is a one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 30-Apr-1998.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ ( I ↾ A):A–1-1-onto→A
Theorem	f1ovi 5321	The identity relation is a one-to-one onto function on the universe. (Contributed by set.mm contributors, 16-May-2004.)
⊢ I :V–1-1-onto→V
Theorem	f1osn 5322	A singleton of an ordered pair is one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 18-May-1998.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ {⟨A, B⟩}:{A}–1-1-onto→{B}
Theorem	f1osng 5323	A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013.)
⊢ ((A ∈ V ∧ B ∈ W) → {⟨A, B⟩}:{A}–1-1-onto→{B})
Theorem	fv2 5324*	Alternate definition of function value. Definition 10.11 of [Quine] p. 68. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 30-Apr-2004.) (Revised by set.mm contributors, 18-Sep-2011.)
⊢ (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, 20-May-1998.)
⊢ (¬ A ∈ V → (F ‘A) = ∅)
Theorem	elfv 5326*	Membership in a function value. (Contributed by set.mm contributors, 30-Apr-2004.)
⊢ (A ∈ (F ‘B) ↔ ∃x(A ∈ x ∧ ∀y(BFy ↔ y = x)))
Theorem	fveq1 5327	Equality theorem for function value. (Contributed by set.mm contributors, 29-Dec-1996.)
⊢ (F = G → (F ‘A) = (G ‘A))
Theorem	fveq2 5328	Equality theorem for function value. (Contributed by set.mm contributors, 29-Dec-1996.)
⊢ (A = B → (F ‘A) = (F ‘B))
Theorem	fveq1i 5329	Equality inference for function value. (Contributed by set.mm contributors, 2-Sep-2003.)
⊢ F = G    ⇒   ⊢ (F ‘A) = (G ‘A)
Theorem	fveq1d 5330	Equality deduction for function value. (Contributed by set.mm contributors, 2-Sep-2003.)
⊢ (φ → F = G)    ⇒   ⊢ (φ → (F ‘A) = (G ‘A))
Theorem	fveq2i 5331	Equality inference for function value. (Contributed by set.mm contributors, 28-Jul-1999.)
⊢ A = B    ⇒   ⊢ (F ‘A) = (F ‘B)
Theorem	fveq2d 5332	Equality deduction for function value. (Contributed by set.mm contributors, 29-May-1999.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (F ‘A) = (F ‘B))
Theorem	fveq12d 5333	Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)
⊢ (φ → F = G)    &   ⊢ (φ → A = B)    ⇒   ⊢ (φ → (F ‘A) = (G ‘B))
Theorem	nffv 5334	Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ ℲxF    &   ⊢ ℲxA    ⇒   ⊢ Ⅎx(F ‘A)
Theorem	nffvd 5335	Deduction version of bound-variable hypothesis builder nffv 5334. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (φ → ℲxF)    &   ⊢ (φ → ℲxA)    ⇒   ⊢ (φ → Ⅎx(F ‘A))
Theorem	csbfv12g 5336	Move class substitution in and out of a function value. (Contributed by NM, 11-Nov-2005.)
⊢ (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, 10-Nov-2005.)
⊢ (A ∈ C → [A / x](F ‘B) = (F ‘[A / x]B))
Theorem	csbfvg 5338*	Substitution for a function value. (Contributed by NM, 1-Jan-2006.)
⊢ (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, 30-Dec-1996.)
⊢ (F ‘A) ∈ V
Theorem	fvif 5340	Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (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, 30-Apr-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (F ‘A) = {x ∣ (∃y(x ∈ y ∧ AFy) ∧ ∃!y AFy)}
Theorem	fvres 5342	The value of a restricted function. (Contributed by set.mm contributors, 2-Aug-1994.) (Revised by set.mm contributors, 16-Feb-2004.)
⊢ (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, 15-Aug-1994.) (Revised by set.mm contributors, 29-May-2007.)
⊢ ((Fun F ∧ G ⊆ F ∧ A ∈ dom G) → (F ‘A) = (G ‘A))
Theorem	tz6.12-1 5344*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.)
⊢ ((AFB ∧ ∃!y AFy) → (F ‘A) = B)
Theorem	tz6.12 5345*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 10-Jul-1994.)
⊢ ((⟨A, B⟩ ∈ F ∧ ∃!y⟨A, y⟩ ∈ F) → (F ‘A) = B)
Theorem	tz6.12-2 5346*	Function value when F is not a function. Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by set.mm contributors, 30-Apr-2004.)
⊢ (¬ ∃!y AFy → (F ‘A) = ∅)
Theorem	tz6.12c 5347*	Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.)
⊢ (∃!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, 30-Apr-2004.) (Revised by set.mm contributors, 6-Apr-2007.)
⊢ (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, 24-Aug-1995.)
⊢ (¬ 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, 26-Apr-1996.)
⊢ 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, 12-Feb-2007.)
⊢ (A ∈ (F ‘B) → B ∈ dom F)
Theorem	nfvres 5352	The value of a non-member of a restriction is the empty set. (Contributed by set.mm contributors, 13-Nov-1995.)
⊢ (¬ 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, 8-Aug-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (¬ Fun (F ↾ {A}) → (F ‘A) = ∅)
Theorem	fv01 5354	Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.)
⊢ (∅ ‘A) = ∅
Theorem	fveqres 5355	Equal values imply equal values in a restriction. (Contributed by set.mm contributors, 13-Nov-1995.)
⊢ ((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, 30-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (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, 19-Jul-1996.)
⊢ (Fun F → (⟨A, B⟩ ∈ F → (F ‘A) = B))
Theorem	fnbrfvb 5358	Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((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, 9-Jan-2015.)
⊢ ((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, 9-Jan-2015.)
⊢ ((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, 9-Jan-2015.)
⊢ ((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, 19-Mar-2014.)
⊢ (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, 29-Jan-2004.)
⊢ (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, 20-Oct-2005.)
⊢ (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, 31-Oct-1995.)
⊢ (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, 20-Nov-2006.)
⊢ ((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, 20-Nov-2006.)
⊢ ((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, 20-Nov-2006.)
⊢ ((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, 22-Oct-2011.) (Contributed by set.mm contributors, 29-Apr-2004.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ ((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, 22-Oct-2011.) (An unnecessary distinct variable restriction was removed by David Abernethy, 17-Dec-2011.) (Contributed by set.mm contributors, 20-Jan-2007.) (Revised by set.mm contributors, 25-Dec-2011.)
⊢ ((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, 12-May-2014.)
⊢ (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, 20-Oct-2005.)
⊢ (F Fn A → ∩x ∈ A (F ‘x) = ∩ran F)
Theorem	fnsnfv 5373	Singleton of function value. (Contributed by set.mm contributors, 22-May-1998.)
⊢ ((F Fn A ∧ B ∈ A) → {(F ‘B)} = (F “ {B}))
Theorem	fnimapr 5374	The image of a pair under a function. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ ((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, 22-May-1998.)
⊢ (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, 22-May-1998.) (Revised by set.mm contributors, 11-May-2005.)
⊢ (Fun F → (F ‘A) = ∪{y ∣ AFy})
Theorem	funfv2f 5377	The value of a function. Version of funfv2 5376 using a bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 19-Feb-2006.)
⊢ Ⅎ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, 7-Nov-2011.)
⊢ (((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, 29-Jun-2013.)
⊢ ((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, 29-Jun-2013.)
⊢ ((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, 27-Jan-1997.)
⊢ ((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, 22-Oct-2011.) (Contributed by set.mm contributors, 9-Oct-2004.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ ((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, 22-Apr-2006.)
⊢ ((Fun G ∧ A ∈ dom G) → ((F ∘ G) ‘A) = (F ‘(G ‘A)))
Theorem	fvco3 5384	Value of a function composition. (Contributed by set.mm contributors, 3-Jan-2004.) (Revised by set.mm contributors, 21-Aug-2006.)
⊢ ((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, 21-Feb-2013.)
⊢ ((∀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 ordered-pair class abstraction. (Contributed by set.mm contributors, 6-Mar-1996.)
⊢ 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 ordered-pair class abstraction. (Contributed by set.mm contributors, 23-Oct-1999.)
⊢ (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 ordered-pair class abstraction. (Contributed by set.mm contributors, 23-Oct-1999.)
⊢ (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 ordered-pair class abstraction. (Contributed by set.mm contributors, 23-Oct-1999.)
⊢ (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 ordered-pair class abstraction, outside of its domain. (Contributed by set.mm contributors, 28-Mar-2008.)
⊢ F = {⟨x, y⟩ ∣ (x ∈ A ∧ φ)}    ⇒   ⊢ (¬ B ∈ A → (F ‘B) = ∅)
Theorem	fvopabg 5391*	The value of a function given by ordered-pair class abstraction. (Contributed by set.mm contributors, 2-Sep-2003.)
⊢ (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, 22-Oct-2011.) (Contributed by set.mm contributors, 3-Aug-1994.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ ((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, 3-Aug-1994.) (Revised by set.mm contributors, 5-Feb-2004.)
⊢ ((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, 2-Sep-2009.)
⊢ ((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, 24-Jul-2014.)
⊢ (φ → 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 bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
⊢ Ⅎ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, 19-Jun-2011.)
⊢ ((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, 3-Aug-1994.) (Revised by set.mm contributors, 6-Feb-2004.)
⊢ (((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, 31-Aug-1999.)
⊢ ((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, 14-Oct-1996.)
⊢ ((Fun F ∧ A ∈ dom F) → ⟨A, (F ‘A)⟩ ∈ F)