P. 63 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6201-6300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fvex 6201	The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by NM, 30-Dec-1996.)
|- ( F ` A ) e. _V
Theorem	fvexi 6202	The value of a class exists. Inference form of fvex 6201. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- A = ( F ` B )   =>    |- A e. _V
Theorem	fvexd 6203	The value of a class exists (as consequent of anything). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> ( F ` A ) e. _V )
Theorem	fvif 6204	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	iffv 6205	Move a conditional outside of a function. (Contributed by Thierry Arnoux, 28-Sep-2018.)
|- ( if ( ph , F , G ) ` A ) = if ( ph , ( F ` A ) , ( G ` A ) )
Theorem	fv3 6206*	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 /\ A F y ) /\ E! y A F y ) }
Theorem	fvres 6207	The value of a restricted function. (Contributed by NM, 2-Aug-1994.)
|- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )
Theorem	fvresd 6208	The value of a restricted function, deduction version of fvres 6207. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A e. B )   =>    |- ( ph -> ( ( F |` B ) ` A ) = ( F ` A ) )
Theorem	funssfv 6209	The value of a member of the domain of a subclass of a function. (Contributed by NM, 15-Aug-1994.)
|- ( ( Fun F /\ G C_ F /\ A e. dom G ) -> ( F ` A ) = ( G ` A ) )
Theorem	tz6.12-1 6210*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.)
|- ( ( A F y /\ E! y A F y ) -> ( F ` A ) = y )
Theorem	tz6.12 6211*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 10-Jul-1994.)
|- ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F ` A ) = y )
Theorem	tz6.12f 6212*	Function value, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 30-Aug-1999.)
|- F/_ y F   =>    |- ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F ` A ) = y )
Theorem	tz6.12c 6213*	Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.)
|- ( E! y A F y -> ( ( F ` A ) = y <-> A F y ) )
Theorem	tz6.12i 6214	Corollary of Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( B =/= (/) -> ( ( F ` A ) = B -> A F B ) )
Theorem	fvbr0 6215	Two possibilities for the behavior of a function value. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|- ( X F ( F ` X ) \/ ( F ` X ) = (/) )
Theorem	fvrn0 6216	A function value is a member of the range plus null. (Contributed by Scott Fenton, 8-Jun-2011.) (Revised by Stefan O'Rear, 3-Jan-2015.)
|- ( F ` X ) e. ( ran F u. { (/) } )
Theorem	fvssunirn 6217	The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( F ` X ) C_ U. ran F
Theorem	ndmfv 6218	The value of a class outside its domain is the empty set. (Contributed by NM, 24-Aug-1995.)
|- ( -. A e. dom F -> ( F ` A ) = (/) )
Theorem	ndmfvrcl 6219	Reverse closure law for function with the empty set not in its domain. (Contributed by NM, 26-Apr-1996.)
|- dom F = S   &    |- -. (/) e. S   =>    |- ( ( F ` A ) e. S -> A e. S )
Theorem	elfvdm 6220	If a function value has a member, the argument belongs to the domain. (Contributed by NM, 12-Feb-2007.)
|- ( A e. ( F ` B ) -> B e. dom F )
Theorem	elfvex 6221	If a function value has a member, the argument is a set. (Contributed by Mario Carneiro, 6-Nov-2015.)
|- ( A e. ( F ` B ) -> B e. _V )
Theorem	elfvexd 6222	If a function value is nonempty, its argument is a set. Deduction form of elfvex 6221. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. ( B ` C ) )   =>    |- ( ph -> C e. _V )
Theorem	eliman0 6223	A non-nul function value is an element of the image of the function. (Contributed by Thierry Arnoux, 25-Jun-2019.)
|- ( ( A e. B /\ -. ( F ` A ) = (/) ) -> ( F ` A ) e. ( F " B ) )
Theorem	nfvres 6224	The value of a non-member of a restriction is the empty set. (Contributed by NM, 13-Nov-1995.)
|- ( -. A e. B -> ( ( F |` B ) ` A ) = (/) )
Theorem	nfunsn 6225	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	fvfundmfvn0 6226	If a class' value at an argument is not the empty set, the argument is contained in the domain of the class, and the class restricted to the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ( F ` A ) =/= (/) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )
Theorem	0fv 6227	Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.)
|- ( (/) ` A ) = (/)
Theorem	fv2prc 6228	A function's value at a function's value at a proper class is the empty set. (Contributed by AV, 8-Apr-2021.)
|- ( -. A e. _V -> ( ( F ` A ) ` B ) = (/) )
Theorem	elfv2ex 6229	If a function value of a function value has a member, the first argument is a set. (Contributed by AV, 8-Apr-2021.)
|- ( A e. ( ( F ` B ) ` C ) -> B e. _V )
Theorem	fveqres 6230	Equal values imply equal values in a restriction. (Contributed by NM, 13-Nov-1995.)
|- ( ( F ` A ) = ( G ` A ) -> ( ( F |` B ) ` A ) = ( ( G |` B ) ` A ) )
Theorem	csbfv12 6231	Move class substitution in and out of a function value. (Contributed by NM, 11-Nov-2005.) (Revised by NM, 20-Aug-2018.)
|- [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B )
Theorem	csbfv2g 6232*	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	csbfv 6233*	Substitution for a function value. (Contributed by NM, 1-Jan-2006.) (Revised by NM, 20-Aug-2018.)
|- [_ A / x ]_ ( F ` x ) = ( F ` A )
Theorem	funbrfv 6234	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 -> ( A F B -> ( F ` A ) = B ) )
Theorem	funopfv 6235	The second element in an ordered pair member of a function is the function's value. (Contributed by NM, 19-Jul-1996.)
|- ( Fun F -> ( <. A , B >. e. F -> ( F ` A ) = B ) )
Theorem	fnbrfvb 6236	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 <-> B F C ) )
Theorem	fnopfvb 6237	Equivalence of function value and ordered pair membership. (Contributed by NM, 7-Nov-1995.)
|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = C <-> <. B , C >. e. F ) )
Theorem	funbrfvb 6238	Equivalence of function value and binary relation. (Contributed by NM, 26-Mar-2006.)
|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = B <-> A F B ) )
Theorem	funopfvb 6239	Equivalence of function value and ordered pair membership. Theorem 4.3(ii) of [Monk1] p. 42. (Contributed by NM, 26-Jan-1997.)
|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = B <-> <. A , B >. e. F ) )
Theorem	funbrfv2b 6240	Function value in terms of a binary relation. (Contributed by Mario Carneiro, 19-Mar-2014.)
|- ( Fun F -> ( A F B <-> ( A e. dom F /\ ( F ` A ) = B ) ) )
Theorem	dffn5 6241*	Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
Theorem	fnrnfv 6242*	The range of a function expressed as a collection of the function's values. (Contributed by NM, 20-Oct-2005.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|- ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )
Theorem	fvelrnb 6243*	A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995.)
|- ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )
Theorem	foelrni 6244*	A member of a surjective function's codomain is a value of the function. (Contributed by Thierry Arnoux, 23-Jan-2020.)
|- ( ( F : A -onto-> B /\ Y e. B ) -> E. x e. A ( F ` x ) = Y )
Theorem	dfimafn 6245*	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 6246*	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 6247*	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 6248*	Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42. (Contributed by NM, 29-Apr-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( Fun F /\ A e. ( F " B ) ) -> E. x e. B ( F ` x ) = A )
Theorem	feqmptd 6249*	Deduction form of dffn5 6241. (Contributed by Mario Carneiro, 8-Jan-2015.)
|- ( ph -> F : A --> B )   =>    |- ( ph -> F = ( x e. A |-> ( F ` x ) ) )
Theorem	feqresmpt 6250*	Express a restricted function as a mapping. (Contributed by Mario Carneiro, 18-May-2016.)
|- ( ph -> F : A --> B )   &    |- ( ph -> C C_ A )   =>    |- ( ph -> ( F |` C ) = ( x e. C |-> ( F ` x ) ) )
Theorem	feqmptdf 6251	Deduction form of dffn5f 6252. (Contributed by Mario Carneiro, 8-Jan-2015.) (Revised by Thierry Arnoux, 10-May-2017.)
|- F/_ x A   &    |- F/_ x F   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> F = ( x e. A |-> ( F ` x ) ) )
Theorem	dffn5f 6252*	Representation of a function in terms of its values. (Contributed by Mario Carneiro, 3-Jul-2015.)
|- F/_ x F   =>    |- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
Theorem	fvelimab 6253*	Function value in an image. (Contributed by NM, 20-Jan-2007.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by David Abernethy, 17-Dec-2011.)
|- ( ( F Fn A /\ B C_ A ) -> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) )
Theorem	fvelimabd 6254*	Deduction form of fvelimab 6253. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F Fn A )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) )
Theorem	fvi 6255	The value of the identity function. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( A e. V -> ( _I ` A ) = A )
Theorem	fviss 6256	The value of the identity function is a subset of the argument. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( _I ` A ) C_ A
Theorem	fniinfv 6257*	The indexed intersection of a function's values is the intersection of its range. (Contributed by NM, 20-Oct-2005.)
|- ( F Fn A -> |^|_ x e. A ( F ` x ) = |^| ran F )
Theorem	fnsnfv 6258	Singleton of function value. (Contributed by NM, 22-May-1998.)
|- ( ( F Fn A /\ B e. A ) -> { ( F ` B ) } = ( F " { B } ) )
Theorem	opabiotafun 6259*	Define a function whose value is "the unique y such that ph ( x , y )". (Contributed by NM, 19-May-2015.)
|- F = { <. x , y >. | { y | ph } = { y } }   =>    |- Fun F
Theorem	opabiotadm 6260*	Define a function whose value is "the unique y such that ph ( x , y )". (Contributed by NM, 16-Nov-2013.)
|- F = { <. x , y >. | { y | ph } = { y } }   =>    |- dom F = { x | E! y ph }
Theorem	opabiota 6261*	Define a function whose value is "the unique y such that ph ( x , y )". (Contributed by NM, 16-Nov-2013.)
|- F = { <. x , y >. | { y | ph } = { y } }   &    |- ( x = B -> ( ph <-> ps ) )   =>    |- ( B e. dom F -> ( F ` B ) = ( iota y ps ) )
Theorem	fnimapr 6262	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	ssimaex 6263*	The existence of a subimage. (Contributed by NM, 8-Apr-2007.)
|- A e. _V   =>    |- ( ( Fun F /\ B C_ ( F " A ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) )
Theorem	ssimaexg 6264*	The existence of a subimage. (Contributed by FL, 15-Apr-2007.)
|- ( ( A e. C /\ Fun F /\ B C_ ( F " A ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) )
Theorem	funfv 6265	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 6266*	The value of a function. Definition of function value in [Enderton] p. 43. (Contributed by NM, 22-May-1998.)
|- ( Fun F -> ( F ` A ) = U. { y | A F y } )
Theorem	funfv2f 6267	The value of a function. Version of funfv2 6266 using a bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 19-Feb-2006.)
|- F/_ y A   &    |- F/_ y F   =>    |- ( Fun F -> ( F ` A ) = U. { y | A F y } )
Theorem	fvun 6268	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 6269	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 6270	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	dffv2 6271	Alternate definition of function value df-fv 5896 that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010.)
|- ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
Theorem	dmfco 6272	Domains of a function composition. (Contributed by NM, 27-Jan-1997.)
|- ( ( Fun G /\ A e. dom G ) -> ( A e. dom ( F o. G ) <-> ( G ` A ) e. dom F ) )
Theorem	fvco2 6273	Value of a function composition. Similar to second part of Theorem 3H of [Enderton] p. 47. (Contributed by NM, 9-Oct-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 16-Oct-2014.)
|- ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
Theorem	fvco 6274	Value of a function composition. Similar to Exercise 5 of [TakeutiZaring] p. 28. (Contributed by NM, 22-Apr-2006.) (Proof shortened by Mario Carneiro, 26-Dec-2014.)
|- ( ( Fun G /\ A e. dom G ) -> ( ( F o. G ) ` A ) = ( F ` ( G ` A ) ) )
Theorem	fvco3 6275	Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.)
|- ( ( G : A --> B /\ C e. A ) -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )
Theorem	fvco4i 6276	Conditions for a composition to be expandable without conditions on the argument. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- (/) = ( F ` (/) )   &    |- Fun G   =>    |- ( ( F o. G ) ` X ) = ( F ` ( G ` X ) )
Theorem	fvopab3g 6277*	Value of a function given by ordered-pair class abstraction. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- ( x e. C -> E! y ph )   &    |- F = { <. x , y >. | ( x e. C /\ ph ) }   =>    |- ( ( A e. C /\ B e. D ) -> ( ( F ` A ) = B <-> ch ) )
Theorem	fvopab3ig 6278*	Value of a function given by ordered-pair class abstraction. (Contributed by NM, 23-Oct-1999.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- ( x e. C -> E* y ph )   &    |- F = { <. x , y >. | ( x e. C /\ ph ) }   =>    |- ( ( A e. C /\ B e. D ) -> ( ch -> ( F ` A ) = B ) )
Theorem	brfvopabrbr 6279*	The binary relation of a function value which is an ordered-pair class abstraction of a restricted binary relation is the restricted binary relation. The first hypothesis can often be obtained by using fvmptopab 6697. (Contributed by AV, 29-Oct-2021.)
|- ( A ` Z ) = { <. x , y >. | ( x ( B ` Z ) y /\ ph ) }   &    |- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )   &    |- Rel ( B ` Z )   =>    |- ( X ( A ` Z ) Y <-> ( X ( B ` Z ) Y /\ ps ) )
Theorem	fvmptg 6280*	Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( x = A -> B = C )   &    |- F = ( x e. D |-> B )   =>    |- ( ( A e. D /\ C e. R ) -> ( F ` A ) = C )
Theorem	fvmpti 6281*	Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
|- ( x = A -> B = C )   &    |- F = ( x e. D |-> B )   =>    |- ( A e. D -> ( F ` A ) = ( _I ` C ) )
Theorem	fvmpt 6282*	Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.)
|- ( x = A -> B = C )   &    |- F = ( x e. D |-> B )   &    |- C e. _V   =>    |- ( A e. D -> ( F ` A ) = C )
Theorem	fvmpt2f 6283	Value of a function given by the "maps to" notation. (Contributed by Thierry Arnoux, 9-Mar-2017.)
|- F/_ x A   =>    |- ( ( x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B )
Theorem	fvtresfn 6284*	Functionality of a tuple-restriction function. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- F = ( x e. B |-> ( x |` V ) )   =>    |- ( X e. B -> ( F ` X ) = ( X |` V ) )
Theorem	fvmpts 6285*	Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- F = ( x e. C |-> B )   =>    |- ( ( A e. C /\ [_ A / x ]_ B e. V ) -> ( F ` A ) = [_ A / x ]_ B )
Theorem	fvmpt3 6286*	Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( x = A -> B = C )   &    |- F = ( x e. D |-> B )   &    |- ( x e. D -> B e. V )   =>    |- ( A e. D -> ( F ` A ) = C )
Theorem	fvmpt3i 6287*	Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( x = A -> B = C )   &    |- F = ( x e. D |-> B )   &    |- B e. _V   =>    |- ( A e. D -> ( F ` A ) = C )
Theorem	fvmptd 6288*	Deduction version of fvmpt 6282. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( ph -> F = ( x e. D |-> B ) )   &    |- ( ( ph /\ x = A ) -> B = C )   &    |- ( ph -> A e. D )   &    |- ( ph -> C e. V )   =>    |- ( ph -> ( F ` A ) = C )
Theorem	mptrcl 6289*	Reverse closure for a mapping: If the function value of a mapping has a member, the argument belongs to the base class of the mapping. (Contributed by AV, 4-Apr-2020.)
|- F = ( x e. A |-> B )   =>    |- ( I e. ( F ` X ) -> X e. A )
Theorem	fvmpt2i 6290*	Value of a function given by the "maps to" notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
|- F = ( x e. A |-> B )   =>    |- ( x e. A -> ( F ` x ) = ( _I ` B ) )
Theorem	fvmpt2 6291*	Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)
|- F = ( x e. A |-> B )   =>    |- ( ( x e. A /\ B e. C ) -> ( F ` x ) = B )
Theorem	fvmptss 6292*	If all the values of the mapping are subsets of a class C, then so is any evaluation of the mapping, even if D is not in the base set A. (Contributed by Mario Carneiro, 13-Feb-2015.)
|- F = ( x e. A |-> B )   =>    |- ( A. x e. A B C_ C -> ( F ` D ) C_ C )
Theorem	fvmpt2d 6293*	Deduction version of fvmpt2 6291. (Contributed by Thierry Arnoux, 8-Dec-2016.)
|- ( ph -> F = ( x e. A |-> B ) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
Theorem	fvmptex 6294*	Express a function F whose value B may not always be a set in terms of another function G for which sethood is guaranteed. (Note that ( _I ` B ) is just shorthand for if ( B e. _V , B , (/) ), and it is always a set by fvex 6201.) Note also that these functions are not the same; wherever B ( C ) is not a set, C is not in the domain of F (so it evaluates to the empty set), but C is in the domain of G, and G ( C ) is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> ( _I ` B ) )   =>    |- ( F ` C ) = ( G ` C )
Theorem	fvmptd3f 6295*	Alternate deduction version of fvmpt 6282 with three non-freeness hypotheses instead of distinct variable conditions. (Contributed by AV, 19-Jan-2022.)
|- ( ph -> A e. D )   &    |- ( ( ph /\ x = A ) -> B e. V )   &    |- ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) )   &    |- F/_ x F   &    |- F/ x ps   &    |- F/ x ph   =>    |- ( ph -> ( F = ( x e. D |-> B ) -> ps ) )
Theorem	fvmptdf 6296*	Alternate deduction version of fvmpt 6282, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) (Proof shortened by AV, 19-Jan-2022.)
|- ( ph -> A e. D )   &    |- ( ( ph /\ x = A ) -> B e. V )   &    |- ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) )   &    |- F/_ x F   &    |- F/ x ps   =>    |- ( ph -> ( F = ( x e. D |-> B ) -> ps ) )
Theorem	fvmptdv 6297*	Alternate deduction version of fvmpt 6282, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> A e. D )   &    |- ( ( ph /\ x = A ) -> B e. V )   &    |- ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) )   =>    |- ( ph -> ( F = ( x e. D |-> B ) -> ps ) )
Theorem	fvmptdv2 6298*	Alternate deduction version of fvmpt 6282, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> A e. D )   &    |- ( ( ph /\ x = A ) -> B e. V )   &    |- ( ( ph /\ x = A ) -> B = C )   =>    |- ( ph -> ( F = ( x e. D |-> B ) -> ( F ` A ) = C ) )
Theorem	mpteqb 6299*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 6311. (Contributed by Mario Carneiro, 14-Nov-2014.)
|- ( A. x e. A B e. V -> ( ( x e. A |-> B ) = ( x e. A |-> C ) <-> A. x e. A B = C ) )
Theorem	fvmptt 6300*	Closed theorem form of fvmpt 6282. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- ( ( A. x ( x = A -> B = C ) /\ F = ( x e. D |-> B ) /\ ( A e. D /\ C e. V ) ) -> ( F ` A ) = C )