P. 60 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5901-6000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cbvmpov 5901*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4059, 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 5902*	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 5903*	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 5904*	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 5905*	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 5906*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
|- Rel dom { <. <. x , y >. , z >. | ph }
Theorem	oprabss 5907*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
|- { <. <. x , y >. , z >. | ph } C_ ( ( _V X. _V ) X. _V )
Theorem	eloprabga 5908*	The law of concretion for operation class abstraction. Compare elopab 4218. (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 5909*	The law of concretion for operation class abstraction. Compare elopab 4218. (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 5910*	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 5911*	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 5912*	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 5913*	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 5914	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 5915	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 5916*	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 5917*	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 5918*	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 5919*	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 5920*	"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 5921*	"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 5922*	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 5923*	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 5924*	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 5925*	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	fovcl 5926	Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
|- F : ( R X. S ) --> C   =>    |- ( ( A e. R /\ B e. S ) -> ( A F B ) e. C )
Theorem	eqfnov 5927*	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 5928*	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 5929*	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 5930*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5928. (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 5931*	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 5932*	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 5933*	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 5934*	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 5935*	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 5936*	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 5937*	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 5938*	The value of an operation class abstraction. Compare ovidi 5939. 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 5939*	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 5940*	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 5941*	The value of an operation class abstraction. Compare ovig 5942. 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 5942*	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 5943*	Value of a function given by the maps-to notation. (This is the operation analog of fvmpt2 5551.) (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 5944*	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 5945*	The value of an operation class abstraction. A version of ovmpog 5955 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 5946*	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 5947*	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 5948*	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 5949*	The value of an operation class abstraction. Variant of ovmpoga 5950 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 5950*	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 5951*	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 5952*	Alternate deduction version of ovmpo 5956, 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 5953*	Alternate deduction version of ovmpo 5956, 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 5954*	Alternate deduction version of ovmpo 5956, 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 5955*	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 5956*	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	ovi3 5957*	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 5958*	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 5959*	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 5960	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 5961	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 5962	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	fovrn 5963	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	fovrnda 5964	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	fovrnd 5965	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 5966*	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 5967*	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 5968	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 5969*	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 5970*	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 5971*	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 5972	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 5973*	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 5974*	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 5975*	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 5976*	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 5977*	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 5978*	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 5979*	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 5980*	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 5981*	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 5982*	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 5983*	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 5984*	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 5985*	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 5986*	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 5987*	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 5988*	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 5989*	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 5990*	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 5991*	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 5992*	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 5993*	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 5994*	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 5995*	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 5996*	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 5997*	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 ) ) )
Theorem	caovdirg 5998*	Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. K ) ) -> ( ( x F y ) G z ) = ( ( x G z ) H ( y G z ) ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S /\ C e. K ) ) -> ( ( A F B ) G C ) = ( ( A G C ) H ( B G C ) ) )
Theorem	caovdird 5999*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. K ) ) -> ( ( x F y ) G z ) = ( ( x G z ) H ( y G z ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. K )   =>    |- ( ph -> ( ( A F B ) G C ) = ( ( A G C ) H ( B G C ) ) )
Theorem	caovdi 6000*	Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) )   =>    |- ( A G ( B F C ) ) = ( ( A G B ) F ( A G C ) )