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	f1ores 5301	The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by set.mm contributors, 25-Mar-1998.)
|- ((F:A-1-1->B /\ C C_ A) -> (F |` C):C-1-1-onto->(F"C))
Theorem	f1orescnv 5302	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 5303	Preimage of an image. (Contributed by set.mm contributors, 30-Sep-2004.)
|- ((F:A-1-1->B /\ C C_ A) -> (`'F"(F"C)) = C)
Theorem	foimacnv 5304	A reverse version of f1imacnv 5303. (Contributed by Jeffrey Hankins, 16-Jul-2009.)
|- ((F:A-onto->B /\ C C_ B) -> (F"(`'F"C)) = C)
Theorem	f1oun 5305	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 i^i C) = (/) /\ (B i^i D) = (/))) -> (F u. G):(A u. C)-1-1-onto->(B u. D))
Theorem	fun11iun 5306*	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 e. _V   =>   |- (A.x e. A (B:D-1-1->S /\ A.y e. A (B C_ C \/ C C_ B)) -> U_x e. A B:U_x e. A D-1-1->S)
Theorem	resdif 5307	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 5308	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 i^i B)):(A i^i B)-1-1-onto->(C i^i D))
Theorem	f1oco 5309	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 o. G):A-1-1-onto->C)
Theorem	f1ococnv2 5310	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 o. `'F) = ( _I |` B))
Theorem	f1ococnv1 5311	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 o. F) = ( _I |` A))
Theorem	f1cnv 5312	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 5313	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
|- (F:A-1-1->B -> (`'F o. F) = ( _I |` A))
Theorem	f1cocnv2 5314	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
|- (F:A-1-1->B -> (F o. `'F) = ( _I |` ran F))
Theorem	ffoss 5315*	Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by set.mm contributors, 10-May-1998.)
|- F e. _V   =>   |- (F:A-->B <-> E.x(F:A-onto->x /\ x C_ B))
Theorem	f11o 5316*	Relationship between one-to-one and one-to-one onto function. (Contributed by set.mm contributors, 4-Apr-1998.)
|- F e. _V   =>   |- (F:A-1-1->B <-> E.x(F:A-1-1-onto->x /\ x C_ B))
Theorem	f10 5317	The empty set maps one-to-one into any class. (Contributed by set.mm contributors, 7-Apr-1998.)
|- (/):(/)-1-1->A
Theorem	f1o00 5318	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 5319	Onto mapping of the empty set. (Contributed by set.mm contributors, 22-Mar-2006.)
|- (F:(/)-onto->A <-> (F = (/) /\ A = (/)))
Theorem	f1o0 5320	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 5321	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 5322	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 5323	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 e. _V   &   |- B e. _V   =>   |- {<.A, B>.}:{A}-1-1-onto->{B}
Theorem	f1osng 5324	A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013.)
|- ((A e. V /\ B e. W) -> {<.A, B>.}:{A}-1-1-onto->{B})
Theorem	fv2 5325*	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) = U.{x | A.y(AFy <-> y = x)}
Theorem	fvprc 5326	A function's value at a proper class is the empty set. (Contributed by set.mm contributors, 20-May-1998.)
|- (-. A e. _V -> (F` A) = (/))
Theorem	elfv 5327*	Membership in a function value. (Contributed by set.mm contributors, 30-Apr-2004.)
|- (A e. (F` B) <-> E.x(A e. x /\ A.y(BFy <-> y = x)))
Theorem	fveq1 5328	Equality theorem for function value. (Contributed by set.mm contributors, 29-Dec-1996.)
|- (F = G -> (F` A) = (G` A))
Theorem	fveq2 5329	Equality theorem for function value. (Contributed by set.mm contributors, 29-Dec-1996.)
|- (A = B -> (F` A) = (F` B))
Theorem	fveq1i 5330	Equality inference for function value. (Contributed by set.mm contributors, 2-Sep-2003.)
|- F = G   =>   |- (F` A) = (G` A)
Theorem	fveq1d 5331	Equality deduction for function value. (Contributed by set.mm contributors, 2-Sep-2003.)
|- (ph -> F = G)   =>   |- (ph -> (F` A) = (G` A))
Theorem	fveq2i 5332	Equality inference for function value. (Contributed by set.mm contributors, 28-Jul-1999.)
|- A = B   =>   |- (F` A) = (F` B)
Theorem	fveq2d 5333	Equality deduction for function value. (Contributed by set.mm contributors, 29-May-1999.)
|- (ph -> A = B)   =>   |- (ph -> (F` A) = (F` B))
Theorem	fveq12d 5334	Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)
|- (ph -> F = G)   &   |- (ph -> A = B)   =>   |- (ph -> (F` A) = (G` B))
Theorem	nffv 5335	Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_xF   &   |- F/_xA   =>   |- F/_x(F` A)
Theorem	nffvd 5336	Deduction version of bound-variable hypothesis builder nffv 5335. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- (ph -> F/_xF)   &   |- (ph -> F/_xA)   =>   |- (ph -> F/_x(F` A))
Theorem	csbfv12g 5337	Move class substitution in and out of a function value. (Contributed by NM, 11-Nov-2005.)
|- (A e. C -> [_A / x]_(F` B) = ([_A / x]_F` [_A / x]_B))
Theorem	csbfv2g 5338*	Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005.)
|- (A e. C -> [_A / x]_(F` B) = (F` [_A / x]_B))
Theorem	csbfvg 5339*	Substitution for a function value. (Contributed by NM, 1-Jan-2006.)
|- (A e. C -> [_A / x]_(F` x) = (F` A))
Theorem	fvex 5340	The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by set.mm contributors, 30-Dec-1996.)
|- (F` A) e. _V
Theorem	fvif 5341	Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- (F` if(ph, A, B)) = if(ph, (F` A), (F` B))
Theorem	fv3 5342*	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 | (E.y(x e. y /\ AFy) /\ E!y AFy)}
Theorem	fvres 5343	The value of a restricted function. (Contributed by set.mm contributors, 2-Aug-1994.) (Revised by set.mm contributors, 16-Feb-2004.)
|- (A e. B -> ((F |` B)` A) = (F` A))
Theorem	funssfv 5344	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 C_ F /\ A e. dom G) -> (F` A) = (G` A))
Theorem	tz6.12-1 5345*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.)
|- ((AFB /\ E!y AFy) -> (F` A) = B)
Theorem	tz6.12 5346*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 10-Jul-1994.)
|- ((<.A, B>. e. F /\ E!y<.A, y>. e. F) -> (F` A) = B)
Theorem	tz6.12-2 5347*	Function value when F is not a function. Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by set.mm contributors, 30-Apr-2004.)
|- (-. E!y AFy -> (F` A) = (/))
Theorem	tz6.12c 5348*	Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.)
|- (E!y AFy -> ((F` A) = B <-> AFB))
Theorem	tz6.12i 5349	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 5350	The value of a class outside its domain is the empty set. (Contributed by set.mm contributors, 24-Aug-1995.)
|- (-. A e. dom F -> (F` A) = (/))
Theorem	ndmfvrcl 5351	Reverse closure law for function with the empty set not in its domain. (Contributed by set.mm contributors, 26-Apr-1996.)
|- dom F = S   &   |- -. (/) e. S   =>   |- ((F` A) e. S -> A e. S)
Theorem	elfvdm 5352	If a function value has a member, the argument belongs to the domain. (Contributed by set.mm contributors, 12-Feb-2007.)
|- (A e. (F` B) -> B e. dom F)
Theorem	nfvres 5353	The value of a non-member of a restriction is the empty set. (Contributed by set.mm contributors, 13-Nov-1995.)
|- (-. A e. B -> ((F |` B)` A) = (/))
Theorem	nfunsn 5354	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 5355	Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.)
|- ((/)` A) = (/)
Theorem	fveqres 5356	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 5357	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 5358	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>. e. F -> (F` A) = B))
Theorem	fnbrfvb 5359	Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ((F Fn A /\ B e. A) -> ((F` B) = C <-> BFC))
Theorem	fnopfvb 5360	Equivalence of function value and ordered pair membership. (Contributed by set.mm contributors, 9-Jan-2015.)
|- ((F Fn A /\ B e. A) -> ((F` B) = C <-> <.B, C>. e. F))
Theorem	funbrfvb 5361	Equivalence of function value and binary relation. (Contributed by set.mm contributors, 9-Jan-2015.)
|- ((Fun F /\ A e. dom F) -> ((F` A) = B <-> AFB))
Theorem	funopfvb 5362	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 e. dom F) -> ((F` A) = B <-> <.A, B>. e. F))
Theorem	funbrfv2b 5363	Function value in terms of a binary relation. (Contributed by Mario Carneiro, 19-Mar-2014.)
|- (Fun F -> (AFB <-> (A e. dom F /\ (F` A) = B)))
Theorem	dffn5 5364*	Representation of a function in terms of its values. (Contributed by set.mm contributors, 29-Jan-2004.)
|- (F Fn A <-> F = {<.x, y>. | (x e. A /\ y = (F` x))})
Theorem	fnrnfv 5365*	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 | E.x e. A y = (F` x)})
Theorem	fvelrnb 5366*	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 e. ran F <-> E.x e. A (F` x) = B))
Theorem	dfimafn 5367*	Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.)
|- ((Fun F /\ A C_ dom F) -> (F"A) = {y | E.x e. A (F` x) = y})
Theorem	dfimafn2 5368*	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 C_ dom F) -> (F"A) = U_x e. A {(F` x)})
Theorem	funimass4 5369*	Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006.)
|- ((Fun F /\ A C_ dom F) -> ((F"A) C_ B <-> A.x e. A (F` x) e. B))
Theorem	fvelima 5370*	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 e. (F"B)) -> E.x e. B (F` x) = A)
Theorem	fvelimab 5371*	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 C_ A) -> (C e. (F"B) <-> E.x e. B (F` x) = C))
Theorem	fniniseg 5372	Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.)
|- (F Fn A -> (C e. (`'F"{B}) <-> (C e. A /\ (F` C) = B)))
Theorem	fniinfv 5373*	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 e. A (F` x) = |^|ran F)
Theorem	fnsnfv 5374	Singleton of function value. (Contributed by set.mm contributors, 22-May-1998.)
|- ((F Fn A /\ B e. A) -> {(F` B)} = (F"{B}))
Theorem	fnimapr 5375	The image of a pair under a function. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- ((F Fn A /\ B e. A /\ C e. A) -> (F"{B, C}) = {(F` B), (F` C)})
Theorem	funfv 5376	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) = U.(F"{A}))
Theorem	funfv2 5377*	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) = U.{y | AFy})
Theorem	funfv2f 5378	The value of a function. Version of funfv2 5377 using a bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 19-Feb-2006.)
|- F/_yA   &   |- F/_yF   =>   |- (Fun F -> (F` A) = U.{y | AFy})
Theorem	fvun 5379	Value of the union of two functions when the domains are separate. (Contributed by FL, 7-Nov-2011.)
|- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> ((F u. G)` A) = ((F` A) u. (G` A)))
Theorem	fvun1 5380	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 i^i B) = (/) /\ X e. A)) -> ((F u. G)` X) = (F` X))
Theorem	fvun2 5381	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 i^i B) = (/) /\ X e. B)) -> ((F u. G)` X) = (G` X))
Theorem	dmfco 5382	Domains of a function composition. (Contributed by set.mm contributors, 27-Jan-1997.)
|- ((Fun G /\ A e. dom G) -> (A e. dom (F o. G) <-> (G` A) e. dom F))
Theorem	fvco2 5383	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 e. A) -> ((F o. G)` C) = (F` (G` C)))
Theorem	fvco 5384	Value of a function composition. Similar to Exercise 5 of [TakeutiZaring] p. 28. (Contributed by set.mm contributors, 22-Apr-2006.)
|- ((Fun G /\ A e. dom G) -> ((F o. G)` A) = (F` (G` A)))
Theorem	fvco3 5385	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 e. A) -> ((F o. G)` C) = (F` (G` C)))
Theorem	fvopab4t 5386*	Closed theorem form of fvopab4 5390. (Contributed by set.mm contributors, 21-Feb-2013.)
|- ((A.xA.y(x = A -> B = C) /\ A.x F = {<.x, y>. | (x e. D /\ y = B)} /\ (A e. D /\ C e. V)) -> (F` A) = C)
Theorem	fvopab3g 5387*	Value of a function given by ordered-pair class abstraction. (Contributed by set.mm contributors, 6-Mar-1996.)
|- B e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (x e. C -> E!yph)   &   |- F = {<.x, y>. | (x e. C /\ ph)}   =>   |- (A e. C -> ((F` A) = B <-> ch))
Theorem	fvopab3ig 5388*	Value of a function given by ordered-pair class abstraction. (Contributed by set.mm contributors, 23-Oct-1999.)
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (x e. C -> E*yph)   &   |- F = {<.x, y>. | (x e. C /\ ph)}   =>   |- ((A e. C /\ B e. D) -> (ch -> (F` A) = B))
Theorem	fvopab4g 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 e. D /\ y = B)}   =>   |- ((A e. D /\ C e. R) -> (F` A) = C)
Theorem	fvopab4 5390*	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 e. D /\ y = B)}   &   |- C e. _V   =>   |- (A e. D -> (F` A) = C)
Theorem	fvopab4ndm 5391*	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 e. A /\ ph)}   =>   |- (-. B e. A -> (F` B) = (/))
Theorem	fvopabg 5392*	The value of a function given by ordered-pair class abstraction. (Contributed by set.mm contributors, 2-Sep-2003.)
|- (x = A -> B = C)   =>   |- ((A e. V /\ C e. W) -> ({<.x, y>. | y = B}` A) = C)
Theorem	eqfnfv 5393*	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 <-> A.x e. A (F` x) = (G` x)))
Theorem	eqfnfv2 5394*	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 /\ A.x e. A (F` x) = (G` x))))
Theorem	eqfnfv3 5395*	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 C_ A /\ A.x e. A (x e. B /\ (F` x) = (G` x)))))
Theorem	eqfnfvd 5396*	Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- (ph -> F Fn A)   &   |- (ph -> G Fn A)   &   |- ((ph /\ x e. A) -> (F` x) = (G` x))   =>   |- (ph -> F = G)
Theorem	eqfnfv2f 5397*	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 5393 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
|- F/_xF   &   |- F/_xG   =>   |- ((F Fn A /\ G Fn A) -> (F = G <-> A.x e. A (F` x) = (G` x)))
Theorem	eqfunfv 5398*	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 /\ A.x e. dom F(F` x) = (G` x))))
Theorem	fvreseq 5399*	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 C_ A) -> ((F |` B) = (G |` B) <-> A.x e. B (F` x) = (G` x)))
Theorem	chfnrn 5400*	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 /\ A.x e. A (F` x) e. x) -> ran F C_ U.A)