P. 61 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	funfvbrb 6001	Two ways to say that A is in the domain of F. (Contributed by Mario Carneiro, 1-May-2014.)
|- ( Fun F -> ( A e. dom F <-> A F ( F ` A ) ) )
Theorem	fvimacnvi 6002	A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.)
|- ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F ` A ) e. B )
Theorem	fvimacnv 6003	The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 5668 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.)
|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )
Theorem	funimass3 6004	A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv 6003 would be the special case of A being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006.)
|- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A C_ ( `' F " B ) ) )
Theorem	funimass5 6005*	A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.)
|- ( ( Fun F /\ A C_ dom F ) -> ( A C_ ( `' F " B ) <-> A. x e. A ( F ` x ) e. B ) )
Theorem	funconstss 6006*	Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.)
|- ( ( Fun F /\ A C_ dom F ) -> ( A. x e. A ( F ` x ) = B <-> A C_ ( `' F " { B } ) ) )
Theorem	fvimacnvALT 6007	Alternate proof of fvimacnv 6003, based on funimass3 6004. If funimass3 6004 is ever proved directly, as opposed to using funimacnv 5666 pointwise, then the proof of funimacnv 5666 should be replaced with this one. (Contributed by Raph Levien, 20-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )
Theorem	elpreima 6008	Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( F Fn A -> ( B e. ( `' F " C ) <-> ( B e. A /\ ( F ` B ) e. C ) ) )
Theorem	fniniseg 6009	Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
|- ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) = B ) ) )
Theorem	fncnvima2 6010*	Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( F Fn A -> ( `' F " B ) = { x e. A | ( F ` x ) e. B } )
Theorem	fniniseg2 6011*	Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( F Fn A -> ( `' F " { B } ) = { x e. A | ( F ` x ) = B } )
Theorem	fnniniseg2OLD 6012*	Support sets of functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) Obsolete version of suppvalfn 6924 as of 22-Apr-2019. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( F Fn A -> ( `' F " ( _V \ { B } ) ) = { x e. A | ( F ` x ) =/= B } )
Theorem	rexsuppOLD 6013*	Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.) Obsolete version of rexsupp 6936 as of 27-May-2019. ( (New usage is discouraged.) (Proof modification is discouraged.)
|- ( F Fn A -> ( E. x e. ( `' F " ( _V \ { Z } ) ) ph <-> E. x e. A ( ( F ` x ) =/= Z /\ ph ) ) )
Theorem	unpreima 6014	Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( Fun F -> ( `' F " ( A u. B ) ) = ( ( `' F " A ) u. ( `' F " B ) ) )
Theorem	inpreima 6015	Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.)
|- ( Fun F -> ( `' F " ( A i^i B ) ) = ( ( `' F " A ) i^i ( `' F " B ) ) )
Theorem	difpreima 6016	Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.)
|- ( Fun F -> ( `' F " ( A \ B ) ) = ( ( `' F " A ) \ ( `' F " B ) ) )
Theorem	respreima 6017	The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( Fun F -> ( `' ( F |` B ) " A ) = ( ( `' F " A ) i^i B ) )
Theorem	iinpreima 6018*	Preimage of an intersection. (Contributed by FL, 16-Apr-2012.)
|- ( ( Fun F /\ A =/= (/) ) -> ( `' F " |^|_ x e. A B ) = |^|_ x e. A ( `' F " B ) )
Theorem	intpreima 6019*	Preimage of an intersection. (Contributed by FL, 28-Apr-2012.)
|- ( ( Fun F /\ A =/= (/) ) -> ( `' F " |^| A ) = |^|_ x e. A ( `' F " x ) )
Theorem	fimacnv 6020	The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.)
|- ( F : A --> B -> ( `' F " B ) = A )
Theorem	suppssOLD 6021*	Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) Obsolete version of suppss 6948 as of 28-May-2019. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F : A --> B )   &    |- ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )   =>    |- ( ph -> ( `' F " ( _V \ { Z } ) ) C_ W )
Theorem	suppssrOLD 6022	A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) Obsolete version of suppssr 6949 as of 28-May-2019. (New usage is discouraged.)
|- ( ph -> F : A --> B )   &    |- ( ph -> ( `' F " ( _V \ { Z } ) ) C_ W )   =>    |- ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )
Theorem	fvn0ssdmfun 6023*	If a class' function values for certain arguments is not the empty set, the arguments are contained in the domain of the class, and the class restricted to the arguments is a function, analogous to fvfundmfvn0 5904. (Contributed by AV, 27-Jan-2020.)
|- ( A. a e. D ( F ` a ) =/= (/) -> ( D C_ dom F /\ Fun ( F |` D ) ) )
Theorem	fnopfv 6024	Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.)
|- ( ( F Fn A /\ B e. A ) -> <. B , ( F ` B ) >. e. F )
Theorem	fvelrn 6025	A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.)
|- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )
Theorem	nelrnfvne 6026	A function value cannot be any element not contained in the range of the function. (Contributed by AV, 28-Jan-2020.)
|- ( ( Fun F /\ X e. dom F /\ Y e/ ran F ) -> ( F ` X ) =/= Y )
Theorem	fveqdmss 6027*	If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the domain of the function is contained in the domain of the class. (Contributed by AV, 28-Jan-2020.)
|- D = dom B   =>    |- ( ( Fun B /\ (/) e/ ran B /\ A. x e. D ( A ` x ) = ( B ` x ) ) -> D C_ dom A )
Theorem	fveqressseq 6028*	If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the class restricted to the domain of the function is the function itself. (Contributed by AV, 28-Jan-2020.)
|- D = dom B   =>    |- ( ( Fun B /\ (/) e/ ran B /\ A. x e. D ( A ` x ) = ( B ` x ) ) -> ( A |` D ) = B )
Theorem	fnfvelrn 6029	A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.)
|- ( ( F Fn A /\ B e. A ) -> ( F ` B ) e. ran F )
Theorem	ffvelrn 6030	A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)
|- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )
Theorem	ffvelrni 6031	A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)
|- F : A --> B   =>    |- ( C e. A -> ( F ` C ) e. B )
Theorem	ffvelrnda 6032	A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> F : A --> B )   =>    |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )
Theorem	ffvelrnd 6033	A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> F : A --> B )   &    |- ( ph -> C e. A )   =>    |- ( ph -> ( F ` C ) e. B )
Theorem	rexrn 6034*	Restricted existential quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)
|- ( x = ( F ` y ) -> ( ph <-> ps ) )   =>    |- ( F Fn A -> ( E. x e. ran F ph <-> E. y e. A ps ) )
Theorem	ralrn 6035*	Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)
|- ( x = ( F ` y ) -> ( ph <-> ps ) )   =>    |- ( F Fn A -> ( A. x e. ran F ph <-> A. y e. A ps ) )
Theorem	elrnrexdm 6036*	For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|- ( Fun F -> ( Y e. ran F -> E. x e. dom F Y = ( F ` x ) ) )
Theorem	elrnrexdmb 6037*	For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|- ( Fun F -> ( Y e. ran F <-> E. x e. dom F Y = ( F ` x ) ) )
Theorem	eldmrexrn 6038*	For any element in the domain of a function there is an element in the range of the function which is the function value for the element of the domain. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|- ( Fun F -> ( Y e. dom F -> E. x e. ran F x = ( F ` Y ) ) )
Theorem	eldmrexrnb 6039*	For any element in the domain of a function, there is an element in the range of the function which is the value of the function at that element. Because of the definition df-fv 5602 of the value of a function, the theorem is only valid in general if the empty set is not contained in the range of the function (the implication "to the right" is always valid). Indeed, with the definition df-fv 5602 of the value of a function, ( F ` Y ) = (/) may mean that the value of F at Y is the empty set or that F is not defined at Y. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|- ( ( Fun F /\ (/) e/ ran F ) -> ( Y e. dom F <-> E. x e. ran F x = ( F ` Y ) ) )
Theorem	fvcofneq 6040*	The values of two function compositions are equal if the values of the composed functions are pairwise equal. (Contributed by AV, 26-Jan-2019.)
|- ( ( G Fn A /\ K Fn B ) -> ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) -> ( ( F o. G ) ` X ) = ( ( H o. K ) ` X ) ) )
Theorem	ralrnmpt 6041*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- F = ( x e. A |-> B )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( A. x e. A B e. V -> ( A. y e. ran F ps <-> A. x e. A ch ) )
Theorem	rexrnmpt 6042*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- F = ( x e. A |-> B )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( A. x e. A B e. V -> ( E. y e. ran F ps <-> E. x e. A ch ) )
Theorem	f0cli 6043	Unconditional closure of a function when the range includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.)
|- F : A --> B   &    |- (/) e. B   =>    |- ( F ` C ) e. B
Theorem	dff2 6044	Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|- ( F : A --> B <-> ( F Fn A /\ F C_ ( A X. B ) ) )
Theorem	dff3 6045*	Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.)
|- ( F : A --> B <-> ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) )
Theorem	dff4 6046*	Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.)
|- ( F : A --> B <-> ( F C_ ( A X. B ) /\ A. x e. A E! y e. B x F y ) )
Theorem	dffo3 6047*	An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.)
|- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
Theorem	dffo4 6048*	Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
|- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A x F y ) )
Theorem	dffo5 6049*	Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
|- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x x F y ) )
Theorem	exfo 6050*	A relation equivalent to the existence of an onto mapping. The right-hand f is not necessarily a function. (Contributed by NM, 20-Mar-2007.)
|- ( E. f f : A -onto-> B <-> E. f ( A. x e. A E! y e. B x f y /\ A. x e. B E. y e. A y f x ) )
Theorem	foelrn 6051*	Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
|- ( ( F : A -onto-> B /\ C e. B ) -> E. x e. A C = ( F ` x ) )
Theorem	foco2 6052	If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( F : B --> C /\ G : A --> B /\ ( F o. G ) : A -onto-> C ) -> F : B -onto-> C )
Theorem	fmpt 6053*	Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- F = ( x e. A |-> C )   =>    |- ( A. x e. A C e. B <-> F : A --> B )
Theorem	f1ompt 6054*	Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|- F = ( x e. A |-> C )   =>    |- ( F : A -1-1-onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E! x e. A y = C ) )
Theorem	fmpti 6055*	Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F = ( x e. A |-> C )   &    |- ( x e. A -> C e. B )   =>    |- F : A --> B
Theorem	fmptd 6056*	Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
|- ( ( ph /\ x e. A ) -> B e. C )   &    |- F = ( x e. A |-> B )   =>    |- ( ph -> F : A --> C )
Theorem	fmptdf 6057*	A version of fmptd 6056 using bound-variable hypothesis instead of a distinct variable condition for ph. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. C )   &    |- F = ( x e. A |-> B )   =>    |- ( ph -> F : A --> C )
Theorem	ffnfv 6058*	A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)
|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
Theorem	ffnfvf 6059	A function maps to a class to which all values belong. This version of ffnfv 6058 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x F   =>    |- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
Theorem	fnfvrnss 6060*	An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.)
|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )
Theorem	rnmptss 6061*	The range of an operation given by the "maps to" notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.)
|- F = ( x e. A |-> B )   =>    |- ( A. x e. A B e. C -> ran F C_ C )
Theorem	fmpt2d 6062*	Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> F = ( x e. A |-> B ) )   &    |- ( ( ph /\ y e. A ) -> ( F ` y ) e. C )   =>    |- ( ph -> F : A --> C )
Theorem	ffvresb 6063*	A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ( Fun F -> ( ( F |` A ) : A --> B <-> A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) )
Theorem	f1oresrab 6064*	Build a bijection between restricted abstract builders, given a bijection between the base classes, deduction version. (Contributed by Thierry Arnoux, 17-Aug-2018.)
|- F = ( x e. A |-> C )   &    |- ( ph -> F : A -1-1-onto-> B )   &    |- ( ( ph /\ x e. A /\ y = C ) -> ( ch <-> ps ) )   =>    |- ( ph -> ( F |` { x e. A | ps } ) : { x e. A | ps } -1-1-onto-> { y e. B | ch } )
Theorem	fmptco 6065*	Composition of two functions expressed as ordered-pair class abstractions. If F has the equation ( x + 2 ) and G the equation ( 3 * z ) then ( G o. F ) has the equation ( 3 * ( x + 2 ) ). (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)
|- ( ( ph /\ x e. A ) -> R e. B )   &    |- ( ph -> F = ( x e. A |-> R ) )   &    |- ( ph -> G = ( y e. B |-> S ) )   &    |- ( y = R -> S = T )   =>    |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )
Theorem	fmptcof 6066*	Version of fmptco 6065 where ph needn't be distinct from x. (Contributed by NM, 27-Dec-2014.)
|- ( ph -> A. x e. A R e. B )   &    |- ( ph -> F = ( x e. A |-> R ) )   &    |- ( ph -> G = ( y e. B |-> S ) )   &    |- ( y = R -> S = T )   =>    |- ( ph -> ( G o. F ) = ( x e. A |-> T ) )
Theorem	fmptcos 6067*	Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( ph -> A. x e. A R e. B )   &    |- ( ph -> F = ( x e. A |-> R ) )   &    |- ( ph -> G = ( y e. B |-> S ) )   =>    |- ( ph -> ( G o. F ) = ( x e. A |-> [_ R / y ]_ S ) )
Theorem	fcompt 6068*	Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
|- ( ( A : D --> E /\ B : C --> D ) -> ( A o. B ) = ( x e. C |-> ( A ` ( B ` x ) ) ) )
Theorem	fcoconst 6069	Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.)
|- ( ( F Fn X /\ Y e. X ) -> ( F o. ( I X. { Y } ) ) = ( I X. { ( F ` Y ) } ) )
Theorem	fsn 6070	A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- ( F : { A } --> { B } <-> F = { <. A , B >. } )
Theorem	fsng 6071	A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012.)
|- ( ( A e. C /\ B e. D ) -> ( F : { A } --> { B } <-> F = { <. A , B >. } ) )
Theorem	fsn2 6072	A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004.)
|- A e. _V   =>    |- ( F : { A } --> B <-> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) )
Theorem	xpsng 6073	The Cartesian product of two singletons. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) = { <. A , B >. } )
Theorem	xpsn 6074	The Cartesian product of two singletons. (Contributed by NM, 4-Nov-2006.)
|- A e. _V   &    |- B e. _V   =>    |- ( { A } X. { B } ) = { <. A , B >. }
Theorem	f1o2sn 6075	A singleton with a nested ordered pair is a 1-1 function of the cartesian product of two singleton onto a singleton. (Contributed by AV, 15-Aug-2019.)
|- ( ( E e. V /\ X e. W ) -> { <. <. E , E >. , X >. } : ( { E } X. { E } ) -1-1-onto-> { X } )
Theorem	residpr 6076	Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018.)
|- ( ( A e. V /\ B e. W ) -> ( _I |` { A , B } ) = { <. A , A >. , <. B , B >. } )
Theorem	dfmpt 6077	Alternate definition for the "maps to" notation df-mpt 4517 (although it requires that B be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.)
|- B e. _V   =>    |- ( x e. A |-> B ) = U_ x e. A { <. x , B >. }
Theorem	fnasrn 6078	A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|- B e. _V   =>    |- ( x e. A |-> B ) = ran ( x e. A |-> <. x , B >. )
Theorem	ressnop0 6079	If A is not in C, then the restriction of a singleton of <. A , B >. to C is null. (Contributed by Scott Fenton, 15-Apr-2011.)
|- ( -. A e. C -> ( { <. A , B >. } |` C ) = (/) )
Theorem	fpr 6080	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )
Theorem	fprg 6081	A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.)
|- ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) /\ A =/= B ) -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )
Theorem	ftpg 6082	A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { <. X , A >. , <. Y , B >. , <. Z , C >. } : { X , Y , Z } --> { A , B , C } )
Theorem	ftp 6083	A function with a domain of three elements. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by Alexander van der Vekens, 23-Jan-2018.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- X e. _V   &    |- Y e. _V   &    |- Z e. _V   &    |- A =/= B   &    |- A =/= C   &    |- B =/= C   =>    |- { <. A , X >. , <. B , Y >. , <. C , Z >. } : { A , B , C } --> { X , Y , Z }
Theorem	fnressn 6084	A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
|- ( ( F Fn A /\ B e. A ) -> ( F |` { B } ) = { <. B , ( F ` B ) >. } )
Theorem	funressn 6085	A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( Fun F -> ( F |` { B } ) C_ { <. B , ( F ` B ) >. } )
Theorem	fressnfv 6086	The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
|- ( ( F Fn A /\ B e. A ) -> ( ( F |` { B } ) : { B } --> C <-> ( F ` B ) e. C ) )
Theorem	fvrnressn 6087	If the value of a function is in the range of the function restricted to the singleton containing the argument, then the value of the function is in the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
|- ( X e. V -> ( ( F ` X ) e. ran ( F |` { X } ) -> ( F ` X ) e. ran F ) )
Theorem	fvressn 6088	The value of a function restricted to the singleton containing the argument equals the value of the function for this argument. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
|- ( X e. V -> ( ( F |` { X } ) ` X ) = ( F ` X ) )
Theorem	fvn0fvelrn 6089	If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
|- ( ( F ` X ) =/= (/) -> ( F ` X ) e. ran F )
Theorem	fvconst 6090	The value of a constant function. (Contributed by NM, 30-May-1999.)
|- ( ( F : A --> { B } /\ C e. A ) -> ( F ` C ) = B )
Theorem	fnsnb 6091	A function whose domain is a singleton can be represented as a singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Revised to add reverse implication. (Revised by NM, 29-Dec-2018.)
|- A e. _V   =>    |- ( F Fn { A } <-> F = { <. A , ( F ` A ) >. } )
Theorem	fmptsn 6092*	Express a singleton function in maps-to notation. (Contributed by NM, 6-Jun-2006.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 28-Feb-2015.)
|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } = ( x e. { A } |-> B ) )
Theorem	fmptsng 6093*	Express a singleton function in maps-to notation. Version of fmptsn 6092 allowing the mapping value to depend on the mapping variable (usual case). (Contributed by AV, 27-Feb-2019.)
|- ( x = A -> B = C )   =>    |- ( ( A e. V /\ C e. W ) -> { <. A , C >. } = ( x e. { A } |-> B ) )
Theorem	fmptsnd 6094*	Express a singleton function in maps-to notation. Deduction form of fmptsng 6093. (Contributed by AV, 4-Aug-2019.)
|- ( ( ph /\ x = A ) -> B = C )   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. W )   =>    |- ( ph -> { <. A , C >. } = ( x e. { A } |-> B ) )
Theorem	fmptap 6095*	Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- A e. _V   &    |- B e. _V   &    |- ( R u. { A } ) = S   &    |- ( x = A -> C = B )   =>    |- ( ( x e. R |-> C ) u. { <. A , B >. } ) = ( x e. S |-> C )
Theorem	fmptapd 6096*	Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> ( R u. { A } ) = S )   &    |- ( ( ph /\ x = A ) -> C = B )   =>    |- ( ph -> ( ( x e. R |-> C ) u. { <. A , B >. } ) = ( x e. S |-> C ) )
Theorem	fmptpr 6097*	Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ( ph /\ x = A ) -> E = C )   &    |- ( ( ph /\ x = B ) -> E = D )   =>    |- ( ph -> { <. A , C >. , <. B , D >. } = ( x e. { A , B } |-> E ) )
Theorem	fvresi 6098	The value of a restricted identity function. (Contributed by NM, 19-May-2004.)
|- ( B e. A -> ( ( _I |` A ) ` B ) = B )
Theorem	fninfp 6099*	Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( F Fn A -> dom ( F i^i _I ) = { x e. A | ( F ` x ) = x } )
Theorem	fnelfp 6100	Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ( F Fn A /\ X e. A ) -> ( X e. dom ( F i^i _I ) <-> ( F ` X ) = X ) )