P. 63 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6201-6300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elrnmpog 6201*	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 6202*	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 6203*	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 6204*	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 6205*	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 6206*	The value of an operation class abstraction. Compare ovidi 6207. 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 6207*	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 6208*	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 6209*	The value of an operation class abstraction. Compare ovig 6210. 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 6210*	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 6211*	Value of a function given by the maps-to notation. (This is the operation analog of fvmpt2 5789.) (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 6212*	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 6213*	The value of an operation class abstraction. A version of ovmpog 6223 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 6214*	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 6215*	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 6216*	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 6217*	The value of an operation class abstraction. Variant of ovmpoga 6218 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 6218*	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 6219*	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 6220*	Alternate deduction version of ovmpo 6224, 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 6221*	Alternate deduction version of ovmpo 6224, 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 6222*	Alternate deduction version of ovmpo 6224, 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 6223*	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 6224*	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 6225*	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 6226*	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 6227*	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 6228*	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 6229	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 6230	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 6231	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 6232	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 6233	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 6234	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 6235*	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 6236*	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 6237	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 6238*	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 6239*	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 6240*	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 6241	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 6242*	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 6243*	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 6244*	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 6245*	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 6246*	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 6247*	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 6248*	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 6249*	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 6250*	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 6251*	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 6252*	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 6253*	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 6254*	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 6255*	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 6256*	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 6257*	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 6258*	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 6259*	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 6260*	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 6261*	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 6262*	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 6263*	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 6264*	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 6265*	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 6266*	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 6267*	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 6268*	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 6269*	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 ) )
Theorem	caov32d 6270*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( 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 /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ph -> ( ( A F B ) F C ) = ( ( A F C ) F B ) )
Theorem	caov12d 6271*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( 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 /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ph -> ( A F ( B F C ) ) = ( B F ( A F C ) ) )
Theorem	caov31d 6272*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( 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 /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ph -> ( ( A F B ) F C ) = ( ( C F B ) F A ) )
Theorem	caov13d 6273*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( 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 /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ph -> ( A F ( B F C ) ) = ( C F ( B F A ) ) )
Theorem	caov4d 6274*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( 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 /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ph -> D e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   =>    |- ( ph -> ( ( A F B ) F ( C F D ) ) = ( ( A F C ) F ( B F D ) ) )
Theorem	caov411d 6275*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( 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 /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ph -> D e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   =>    |- ( ph -> ( ( A F B ) F ( C F D ) ) = ( ( C F B ) F ( A F D ) ) )
Theorem	caov42d 6276*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( 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 /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ph -> D e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   =>    |- ( ph -> ( ( A F B ) F ( C F D ) ) = ( ( A F C ) F ( D F B ) ) )
Theorem	caov32 6277*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( ( A F B ) F C ) = ( ( A F C ) F B )
Theorem	caov12 6278*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( A F ( B F C ) ) = ( B F ( A F C ) )
Theorem	caov31 6279*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( ( A F B ) F C ) = ( ( C F B ) F A )
Theorem	caov13 6280*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( A F ( B F C ) ) = ( C F ( B F A ) )
Theorem	caovdilemd 6281*	Lemma used by real number construction. (Contributed by Jim Kingdon, 16-Sep-2019.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) = ( y G x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) G z ) = ( ( x G z ) F ( y G z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) e. S )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ph -> D e. S )   &    |- ( ph -> H e. S )   =>    |- ( ph -> ( ( ( A G C ) F ( B G D ) ) G H ) = ( ( A G ( C G H ) ) F ( B G ( D G H ) ) ) )
Theorem	caovlem2d 6282*	Rearrangement of expression involving multiplication ( G) and addition ( F). (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) = ( y G x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) G z ) = ( ( x G z ) F ( y G z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) e. S )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ph -> D e. S )   &    |- ( ph -> H e. S )   &    |- ( ph -> R e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   =>    |- ( ph -> ( ( ( ( A G C ) F ( B G D ) ) G H ) F ( ( ( A G D ) F ( B G C ) ) G R ) ) = ( ( A G ( ( C G H ) F ( D G R ) ) ) F ( B G ( ( C G R ) F ( D G H ) ) ) ) )
Theorem	caovimo 6283*	Uniqueness of inverse element in commutative, associative operation with identity. The identity element is B. (Contributed by Jim Kingdon, 18-Sep-2019.)
|- B e. S   &    |- ( ( x e. S /\ y e. S ) -> ( x F y ) = ( y F x ) )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( x e. S -> ( x F B ) = x )   =>    |- ( A e. S -> E* w ( w e. S /\ ( A F w ) = B ) )
2.6.12  Maps-to notation
Theorem	elmpocl 6284*	If a two-parameter class is inhabited, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( X e. ( S F T ) -> ( S e. A /\ T e. B ) )
Theorem	elmpocl1 6285*	If a two-parameter class is inhabited, the first argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( X e. ( S F T ) -> S e. A )
Theorem	elmpocl2 6286*	If a two-parameter class is inhabited, the second argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( X e. ( S F T ) -> T e. B )
Theorem	elovmpod 6287*	Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.) Variant of elovmpo 6288 in deduction form. (Revised by AV, 20-Apr-2025.)
|- O = ( a e. A , b e. B |-> C )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. B )   &    |- ( ph -> D e. V )   &    |- ( ( a = X /\ b = Y ) -> C = D )   =>    |- ( ph -> ( E e. ( X O Y ) <-> E e. D ) )
Theorem	elovmpo 6288*	Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.)
|- D = ( a e. A , b e. B |-> C )   &    |- C e. _V   &    |- ( ( a = X /\ b = Y ) -> C = E )   =>    |- ( F e. ( X D Y ) <-> ( X e. A /\ Y e. B /\ F e. E ) )
Theorem	elovmporab 6289*	Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- O = ( x e. _V , y e. _V |-> { z e. M | ph } )   &    |- ( ( X e. _V /\ Y e. _V ) -> M e. _V )   =>    |- ( Z e. ( X O Y ) -> ( X e. _V /\ Y e. _V /\ Z e. M ) )
Theorem	elovmporab1w 6290*	Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by GG, 26-Jan-2024.)
|- O = ( x e. _V , y e. _V |-> { z e. [_ x / m ]_ M | ph } )   &    |- ( ( X e. _V /\ Y e. _V ) -> [_ X / m ]_ M e. _V )   =>    |- ( Z e. ( X O Y ) -> ( X e. _V /\ Y e. _V /\ Z e. [_ X / m ]_ M ) )
Theorem	relmptopab 6291*	Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 7-Aug-2014.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- F = ( x e. A |-> { <. y , z >. | ph } )   =>    |- Rel ( F ` B )
Theorem	f1ocnvd 6292*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- F = ( x e. A |-> C )   &    |- ( ( ph /\ x e. A ) -> C e. W )   &    |- ( ( ph /\ y e. B ) -> D e. X )   &    |- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )   =>    |- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )
Theorem	f1od 6293*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
|- F = ( x e. A |-> C )   &    |- ( ( ph /\ x e. A ) -> C e. W )   &    |- ( ( ph /\ y e. B ) -> D e. X )   &    |- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )   =>    |- ( ph -> F : A -1-1-onto-> B )
Theorem	f1ocnv2d 6294*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- F = ( x e. A |-> C )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ y e. B ) -> D e. A )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )   =>    |- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )
Theorem	f1o2d 6295*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
|- F = ( x e. A |-> C )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ y e. B ) -> D e. A )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )   =>    |- ( ph -> F : A -1-1-onto-> B )
Theorem	f1opw2 6296*	A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw 6297 avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015.)
|- ( ph -> F : A -1-1-onto-> B )   &    |- ( ph -> ( `' F " a ) e. _V )   &    |- ( ph -> ( F " b ) e. _V )   =>    |- ( ph -> ( b e. ~P A |-> ( F " b ) ) : ~P A -1-1-onto-> ~P B )
Theorem	f1opw 6297*	A one-to-one mapping induces a one-to-one mapping on power sets. (Contributed by Stefan O'Rear, 18-Nov-2014.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( F : A -1-1-onto-> B -> ( b e. ~P A |-> ( F " b ) ) : ~P A -1-1-onto-> ~P B )
Theorem	f1o3d 6298*	Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.)
|- ( ph -> F = ( x e. A |-> C ) )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ y e. B ) -> D e. A )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )   =>    |- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )
Theorem	suppssov1 6299*	Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- ( ph -> ( `' ( x e. D |-> A ) " ( _V \ { Y } ) ) C_ L )   &    |- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )   &    |- ( ( ph /\ x e. D ) -> A e. V )   &    |- ( ( ph /\ x e. D ) -> B e. R )   =>    |- ( ph -> ( `' ( x e. D |-> ( A O B ) ) " ( _V \ { Z } ) ) C_ L )
2.6.13  Function operation
Syntax	cof 6300	Extend class notation to include mapping of an operation to a function operation.
class oF R