P. 61 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cbvmpo 6001*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
|- F/_ z C   &    |- F/_ w C   &    |- F/_ x D   &    |- F/_ y D   &    |- ( ( x = z /\ y = w ) -> C = D )   =>    |- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )
Theorem	cbvmpov 6002*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4128, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
|- ( x = z -> C = E )   &    |- ( y = w -> E = D )   =>    |- ( x e. A , y e. B |-> C ) = ( z e. A , w e. B |-> D )
Theorem	dmoprab 6003*	The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- dom { <. <. x , y >. , z >. | ph } = { <. x , y >. | E. z ph }
Theorem	dmoprabss 6004*	The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)
|- dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )
Theorem	rnoprab 6005*	The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
|- ran { <. <. x , y >. , z >. | ph } = { z | E. x E. y ph }
Theorem	rnoprab2 6006*	The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
|- ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } = { z | E. x e. A E. y e. B ph }
Theorem	reldmoprab 6007*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
|- Rel dom { <. <. x , y >. , z >. | ph }
Theorem	oprabss 6008*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
|- { <. <. x , y >. , z >. | ph } C_ ( ( _V X. _V ) X. _V )
Theorem	eloprabga 6009*	The law of concretion for operation class abstraction. Compare elopab 4292. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )   =>    |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) )
Theorem	eloprabg 6010*	The law of concretion for operation class abstraction. Compare elopab 4292. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- ( z = C -> ( ch <-> th ) )   =>    |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> th ) )
Theorem	ssoprab2i 6011*	Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( ph -> ps )   =>    |- { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps }
Theorem	mpov 6012*	Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
|- ( x e. _V , y e. _V |-> C ) = { <. <. x , y >. , z >. | z = C }
Theorem	mpomptx 6013*	Express a two-argument function as a one-argument function, or vice-versa. In this version B ( x ) is not assumed to be constant w.r.t x. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( z = <. x , y >. -> C = D )   =>    |- ( z e. U_ x e. A ( { x } X. B ) |-> C ) = ( x e. A , y e. B |-> D )
Theorem	mpompt 6014*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)
|- ( z = <. x , y >. -> C = D )   =>    |- ( z e. ( A X. B ) |-> C ) = ( x e. A , y e. B |-> D )
Theorem	mpodifsnif 6015	A mapping with two arguments with the first argument from a difference set with a singleton and a conditional as result. (Contributed by AV, 13-Feb-2019.)
|- ( i e. ( A \ { X } ) , j e. B |-> if ( i = X , C , D ) ) = ( i e. ( A \ { X } ) , j e. B |-> D )
Theorem	mposnif 6016	A mapping with two arguments with the first argument from a singleton and a conditional as result. (Contributed by AV, 14-Feb-2019.)
|- ( i e. { X } , j e. B |-> if ( i = X , C , D ) ) = ( i e. { X } , j e. B |-> C )
Theorem	fconstmpo 6017*	Representation of a constant operation using the mapping operation. (Contributed by SO, 11-Jul-2018.)
|- ( ( A X. B ) X. { C } ) = ( x e. A , y e. B |-> C )
Theorem	resoprab 6018*	Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)
|- ( { <. <. x , y >. , z >. | ph } |` ( A X. B ) ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }
Theorem	resoprab2 6019*	Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( C C_ A /\ D C_ B ) -> ( { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } |` ( C X. D ) ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ph ) } )
Theorem	resmpo 6020*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
|- ( ( C C_ A /\ D C_ B ) -> ( ( x e. A , y e. B |-> E ) |` ( C X. D ) ) = ( x e. C , y e. D |-> E ) )
Theorem	funoprabg 6021*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
|- ( A. x A. y E* z ph -> Fun { <. <. x , y >. , z >. | ph } )
Theorem	funoprab 6022*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
|- E* z ph   =>    |- Fun { <. <. x , y >. , z >. | ph }
Theorem	fnoprabg 6023*	Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)
|- ( A. x A. y ( ph -> E! z ps ) -> { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph } )
Theorem	mpofun 6024*	The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)
|- F = ( x e. A , y e. B |-> C )   =>    |- Fun F
Theorem	fnoprab 6025*	Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
|- ( ph -> E! z ps )   =>    |- { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph }
Theorem	ffnov 6026*	An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.)
|- ( F : ( A X. B ) --> C <-> ( F Fn ( A X. B ) /\ A. x e. A A. y e. B ( x F y ) e. C ) )
Theorem	fovcld 6027	Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Revised by Thierry Arnoux, 17-Feb-2017.)
|- ( ph -> F : ( R X. S ) --> C )   =>    |- ( ( ph /\ A e. R /\ B e. S ) -> ( A F B ) e. C )
Theorem	fovcl 6028	Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Proof shortened by AV, 9-Mar-2025.)
|- F : ( R X. S ) --> C   =>    |- ( ( A e. R /\ B e. S ) -> ( A F B ) e. C )
Theorem	eqfnov 6029*	Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.)
|- ( ( F Fn ( A X. B ) /\ G Fn ( C X. D ) ) -> ( F = G <-> ( ( A X. B ) = ( C X. D ) /\ A. x e. A A. y e. B ( x F y ) = ( x G y ) ) ) )
Theorem	eqfnov2 6030*	Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.)
|- ( ( F Fn ( A X. B ) /\ G Fn ( A X. B ) ) -> ( F = G <-> A. x e. A A. y e. B ( x F y ) = ( x G y ) ) )
Theorem	fnovim 6031*	Representation of a function in terms of its values. (Contributed by Jim Kingdon, 16-Jan-2019.)
|- ( F Fn ( A X. B ) -> F = ( x e. A , y e. B |-> ( x F y ) ) )
Theorem	mpo2eqb 6032*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 6030. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( A. x e. A A. y e. B C e. V -> ( ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) <-> A. x e. A A. y e. B C = D ) )
Theorem	rnmpo 6033*	The range of an operation given by the maps-to notation. (Contributed by FL, 20-Jun-2011.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ran F = { z | E. x e. A E. y e. B z = C }
Theorem	reldmmpo 6034*	The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- F = ( x e. A , y e. B |-> C )   =>    |- Rel dom F
Theorem	elrnmpog 6035*	Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( D e. V -> ( D e. ran F <-> E. x e. A E. y e. B D = C ) )
Theorem	elrnmpo 6036*	Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- F = ( x e. A , y e. B |-> C )   &    |- C e. _V   =>    |- ( D e. ran F <-> E. x e. A E. y e. B D = C )
Theorem	ralrnmpo 6037*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
|- F = ( x e. A , y e. B |-> C )   &    |- ( z = C -> ( ph <-> ps ) )   =>    |- ( A. x e. A A. y e. B C e. V -> ( A. z e. ran F ph <-> A. x e. A A. y e. B ps ) )
Theorem	rexrnmpo 6038*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
|- F = ( x e. A , y e. B |-> C )   &    |- ( z = C -> ( ph <-> ps ) )   =>    |- ( A. x e. A A. y e. B C e. V -> ( E. z e. ran F ph <-> E. x e. A E. y e. B ps ) )
Theorem	ovid 6039*	The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( ( x e. R /\ y e. S ) -> E! z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }   =>    |- ( ( x e. R /\ y e. S ) -> ( ( x F y ) = z <-> ph ) )
Theorem	ovidig 6040*	The value of an operation class abstraction. Compare ovidi 6041. The condition ( x e. R /\ y e. S ) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- E* z ph   &    |- F = { <. <. x , y >. , z >. | ph }   =>    |- ( ph -> ( x F y ) = z )
Theorem	ovidi 6041*	The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( ( x e. R /\ y e. S ) -> E* z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }   =>    |- ( ( x e. R /\ y e. S ) -> ( ph -> ( x F y ) = z ) )
Theorem	ov 6042*	The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- C e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- ( z = C -> ( ch <-> th ) )   &    |- ( ( x e. R /\ y e. S ) -> E! z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }   =>    |- ( ( A e. R /\ B e. S ) -> ( ( A F B ) = C <-> th ) )
Theorem	ovigg 6043*	The value of an operation class abstraction. Compare ovig 6044. The condition ( x e. R /\ y e. S ) is been removed. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )   &    |- E* z ph   &    |- F = { <. <. x , y >. , z >. | ph }   =>    |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ps -> ( A F B ) = C ) )
Theorem	ovig 6044*	The value of an operation class abstraction (weak version). (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 14-Sep-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )   &    |- ( ( x e. R /\ y e. S ) -> E* z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }   =>    |- ( ( A e. R /\ B e. S /\ C e. D ) -> ( ps -> ( A F B ) = C ) )
Theorem	ovmpt4g 6045*	Value of a function given by the maps-to notation. (This is the operation analog of fvmpt2 5645.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( x e. A /\ y e. B /\ C e. V ) -> ( x F y ) = C )
Theorem	ovmpos 6046*	Value of a function given by the maps-to notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. D /\ [_ A / x ]_ [_ B / y ]_ R e. V ) -> ( A F B ) = [_ A / x ]_ [_ B / y ]_ R )
Theorem	ov2gf 6047*	The value of an operation class abstraction. A version of ovmpog 6057 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- F/_ x A   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x G   &    |- F/_ y S   &    |- ( x = A -> R = G )   &    |- ( y = B -> G = S )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )
Theorem	ovmpodxf 6048*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ( ph /\ x = A ) -> D = L )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. L )   &    |- ( ph -> S e. X )   &    |- F/ x ph   &    |- F/ y ph   &    |- F/_ y A   &    |- F/_ x B   &    |- F/_ x S   &    |- F/_ y S   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpodx 6049*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ( ph /\ x = A ) -> D = L )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. L )   &    |- ( ph -> S e. X )   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpod 6050*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. D )   &    |- ( ph -> S e. X )   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpox 6051*	The value of an operation class abstraction. Variant of ovmpoga 6052 which does not require D and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|- ( ( x = A /\ y = B ) -> R = S )   &    |- ( x = A -> D = L )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. L /\ S e. H ) -> ( A F B ) = S )
Theorem	ovmpoga 6052*	Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> R = S )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )
Theorem	ovmpoa 6053*	Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> R = S )   &    |- F = ( x e. C , y e. D |-> R )   &    |- S e. _V   =>    |- ( ( A e. C /\ B e. D ) -> ( A F B ) = S )
Theorem	ovmpodf 6054*	Alternate deduction version of ovmpo 6058, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> A e. C )   &    |- ( ( ph /\ x = A ) -> B e. D )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A F B ) = R -> ps ) )   &    |- F/_ x F   &    |- F/ x ps   &    |- F/_ y F   &    |- F/ y ps   =>    |- ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ps ) )
Theorem	ovmpodv 6055*	Alternate deduction version of ovmpo 6058, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> A e. C )   &    |- ( ( ph /\ x = A ) -> B e. D )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A F B ) = R -> ps ) )   =>    |- ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ps ) )
Theorem	ovmpodv2 6056*	Alternate deduction version of ovmpo 6058, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> A e. C )   &    |- ( ( ph /\ x = A ) -> B e. D )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   =>    |- ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ( A F B ) = S ) )
Theorem	ovmpog 6057*	Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( x = A -> R = G )   &    |- ( y = B -> G = S )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )
Theorem	ovmpo 6058*	Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( x = A -> R = G )   &    |- ( y = B -> G = S )   &    |- F = ( x e. C , y e. D |-> R )   &    |- S e. _V   =>    |- ( ( A e. C /\ B e. D ) -> ( A F B ) = S )
Theorem	fvmpopr2d 6059*	Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024.)
|- ( ph -> F = ( a e. A , b e. B |-> C ) )   &    |- ( ph -> P = <. a , b >. )   &    |- ( ( ph /\ a e. A /\ b e. B ) -> C e. V )   =>    |- ( ( ph /\ a e. A /\ b e. B ) -> ( F ` P ) = C )
Theorem	ovi3 6060*	The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
|- ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> S e. ( H X. H ) )   &    |- ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> R = S )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) }   =>    |- ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( <. A , B >. F <. C , D >. ) = S )
Theorem	ov6g 6061*	The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)
|- ( <. x , y >. = <. A , B >. -> R = S )   &    |- F = { <. <. x , y >. , z >. | ( <. x , y >. e. C /\ z = R ) }   =>    |- ( ( ( A e. G /\ B e. H /\ <. A , B >. e. C ) /\ S e. J ) -> ( A F B ) = S )
Theorem	ovg 6062*	The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- ( z = C -> ( ch <-> th ) )   &    |- ( ( ta /\ ( x e. R /\ y e. S ) ) -> E! z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }   =>    |- ( ( ta /\ ( A e. R /\ B e. S /\ C e. D ) ) -> ( ( A F B ) = C <-> th ) )
Theorem	ovres 6063	The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|- ( ( A e. C /\ B e. D ) -> ( A ( F |` ( C X. D ) ) B ) = ( A F B ) )
Theorem	ovresd 6064	Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) )
Theorem	oprssov 6065	The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.)
|- ( ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) /\ ( A e. C /\ B e. D ) ) -> ( A F B ) = ( A G B ) )
Theorem	fovcdm 6066	An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
|- ( ( F : ( R X. S ) --> C /\ A e. R /\ B e. S ) -> ( A F B ) e. C )
Theorem	fovcdmda 6067	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> F : ( R X. S ) --> C )   =>    |- ( ( ph /\ ( A e. R /\ B e. S ) ) -> ( A F B ) e. C )
Theorem	fovcdmd 6068	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> F : ( R X. S ) --> C )   &    |- ( ph -> A e. R )   &    |- ( ph -> B e. S )   =>    |- ( ph -> ( A F B ) e. C )
Theorem	fnrnov 6069*	The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)
|- ( F Fn ( A X. B ) -> ran F = { z | E. x e. A E. y e. B z = ( x F y ) } )
Theorem	foov 6070*	An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.)
|- ( F : ( A X. B ) -onto-> C <-> ( F : ( A X. B ) --> C /\ A. z e. C E. x e. A E. y e. B z = ( x F y ) ) )
Theorem	fnovrn 6071	An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
|- ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( C F D ) e. ran F )
Theorem	ovelrn 6072*	A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
|- ( F Fn ( A X. B ) -> ( C e. ran F <-> E. x e. A E. y e. B C = ( x F y ) ) )
Theorem	funimassov 6073*	Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- ( ( Fun F /\ ( A X. B ) C_ dom F ) -> ( ( F " ( A X. B ) ) C_ C <-> A. x e. A A. y e. B ( x F y ) e. C ) )
Theorem	ovelimab 6074*	Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
|- ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( D e. ( F " ( B X. C ) ) <-> E. x e. B E. y e. C D = ( x F y ) ) )
Theorem	ovconst2 6075	The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
|- C e. _V   =>    |- ( ( R e. A /\ S e. B ) -> ( R ( ( A X. B ) X. { C } ) S ) = C )
Theorem	caovclg 6076*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
|- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x F y ) e. E )   =>    |- ( ( ph /\ ( A e. C /\ B e. D ) ) -> ( A F B ) e. E )
Theorem	caovcld 6077*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x F y ) e. E )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. D )   =>    |- ( ph -> ( A F B ) e. E )
Theorem	caovcl 6078*	Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|- ( ( x e. S /\ y e. S ) -> ( x F y ) e. S )   =>    |- ( ( A e. S /\ B e. S ) -> ( A F B ) e. S )
Theorem	caovcomg 6079*	Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S ) ) -> ( A F B ) = ( B F A ) )
Theorem	caovcomd 6080*	Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   =>    |- ( ph -> ( A F B ) = ( B F A ) )
Theorem	caovcom 6081*	Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
|- A e. _V   &    |- B e. _V   &    |- ( x F y ) = ( y F x )   =>    |- ( A F B ) = ( B F A )
Theorem	caovassg 6082*	Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
Theorem	caovassd 6083*	Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
Theorem	caovass 6084*	Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( ( A F B ) F C ) = ( A F ( B F C ) )
Theorem	caovcang 6085*	Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )   =>    |- ( ( ph /\ ( A e. T /\ B e. S /\ C e. S ) ) -> ( ( A F B ) = ( A F C ) <-> B = C ) )
Theorem	caovcand 6086*	Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( ( A F B ) = ( A F C ) <-> B = C ) )
Theorem	caovcanrd 6087*	Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   =>    |- ( ph -> ( ( B F A ) = ( C F A ) <-> B = C ) )
Theorem	caovcan 6088*	Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.)
|- C e. _V   &    |- ( ( x e. S /\ y e. S ) -> ( ( x F y ) = ( x F z ) -> y = z ) )   =>    |- ( ( A e. S /\ B e. S ) -> ( ( A F B ) = ( A F C ) -> B = C ) )
Theorem	caovordig 6089*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y -> ( z F x ) R ( z F y ) ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( A R B -> ( C F A ) R ( C F B ) ) )
Theorem	caovordid 6090*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y -> ( z F x ) R ( z F y ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( A R B -> ( C F A ) R ( C F B ) ) )
Theorem	caovordg 6091*	Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( A R B <-> ( C F A ) R ( C F B ) ) )
Theorem	caovordd 6092*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( A R B <-> ( C F A ) R ( C F B ) ) )
Theorem	caovord2d 6093*	Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   =>    |- ( ph -> ( A R B <-> ( A F C ) R ( B F C ) ) )
Theorem	caovord3d 6094*	Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ph -> D e. S )   =>    |- ( ph -> ( ( A F B ) = ( C F D ) -> ( A R C <-> D R B ) ) )
Theorem	caovord 6095*	Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.)
|- A e. _V   &    |- B e. _V   &    |- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )   =>    |- ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )
Theorem	caovord2 6096*	Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996.)
|- A e. _V   &    |- B e. _V   &    |- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   =>    |- ( C e. S -> ( A R B <-> ( A F C ) R ( B F C ) ) )
Theorem	caovord3 6097*	Ordering law. (Contributed by NM, 29-Feb-1996.)
|- A e. _V   &    |- B e. _V   &    |- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- D e. _V   =>    |- ( ( ( B e. S /\ C e. S ) /\ ( A F B ) = ( C F D ) ) -> ( A R C <-> D R B ) )
Theorem	caovdig 6098*	Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
|- ( ( ph /\ ( x e. K /\ y e. S /\ z e. S ) ) -> ( x G ( y F z ) ) = ( ( x G y ) H ( x G z ) ) )   =>    |- ( ( ph /\ ( A e. K /\ B e. S /\ C e. S ) ) -> ( A G ( B F C ) ) = ( ( A G B ) H ( A G C ) ) )
Theorem	caovdid 6099*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. K /\ y e. S /\ z e. S ) ) -> ( x G ( y F z ) ) = ( ( x G y ) H ( x G z ) ) )   &    |- ( ph -> A e. K )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( A G ( B F C ) ) = ( ( A G B ) H ( A G C ) ) )
Theorem	caovdir2d 6100*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) = ( y G x ) )   =>    |- ( ph -> ( ( A F B ) G C ) = ( ( A G C ) F ( B G C ) ) )