P. 68 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6701-6800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfoprab2 6701*	Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- { <. <. x , y >. , z >. | ph } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) }
Theorem	reloprab 6702*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
|- Rel { <. <. x , y >. , z >. | ph }
Theorem	oprabv 6703*	If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
|- ( <. X , Y >. { <. <. x , y >. , z >. | ph } Z -> ( X e. _V /\ Y e. _V /\ Z e. _V ) )
Theorem	nfoprab1 6704	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- F/_ x { <. <. x , y >. , z >. | ph }
Theorem	nfoprab2 6705	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.)
|- F/_ y { <. <. x , y >. , z >. | ph }
Theorem	nfoprab3 6706	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
|- F/_ z { <. <. x , y >. , z >. | ph }
Theorem	nfoprab 6707*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
|- F/ w ph   =>    |- F/_ w { <. <. x , y >. , z >. | ph }
Theorem	oprabbid 6708*	Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- F/ x ph   &    |- F/ y ph   &    |- F/ z ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. <. x , y >. , z >. | ps } = { <. <. x , y >. , z >. | ch } )
Theorem	oprabbidv 6709*	Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. <. x , y >. , z >. | ps } = { <. <. x , y >. , z >. | ch } )
Theorem	oprabbii 6710*	Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( ph <-> ps )   =>    |- { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , z >. | ps }
Theorem	ssoprab2 6711	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 5001. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
|- ( A. x A. y A. z ( ph -> ps ) -> { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } )
Theorem	ssoprab2b 6712	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 5002. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
|- ( { <. <. x , y >. , z >. | ph } C_ { <. <. x , y >. , z >. | ps } <-> A. x A. y A. z ( ph -> ps ) )
Theorem	eqoprab2b 6713	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 5005. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , z >. | ps } <-> A. x A. y A. z ( ph <-> ps ) )
Theorem	mpt2eq123 6714*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
|- ( ( A = D /\ A. x e. A ( B = E /\ A. y e. B C = F ) ) -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )
Theorem	mpt2eq12 6715*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( ( A = C /\ B = D ) -> ( x e. A , y e. B |-> E ) = ( x e. C , y e. D |-> E ) )
Theorem	mpt2eq123dva 6716*	An equality deduction for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> A = D )   &    |- ( ( ph /\ x e. A ) -> B = E )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = F )   =>    |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )
Theorem	mpt2eq123dv 6717*	An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)
|- ( ph -> A = D )   &    |- ( ph -> B = E )   &    |- ( ph -> C = F )   =>    |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )
Theorem	mpt2eq123i 6718	An equality inference for the maps to notation. (Contributed by NM, 15-Jul-2013.)
|- A = D   &    |- B = E   &    |- C = F   =>    |- ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F )
Theorem	mpt2eq3dva 6719*	Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.)
|- ( ( ph /\ x e. A /\ y e. B ) -> C = D )   =>    |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )
Theorem	mpt2eq3ia 6720	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( ( x e. A /\ y e. B ) -> C = D )   =>    |- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D )
Theorem	mpt2eq3dv 6721*	An equality deduction for the maps to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.)
|- ( ph -> C = D )   =>    |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )
Theorem	nfmpt21 6722	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
|- F/_ x ( x e. A , y e. B |-> C )
Theorem	nfmpt22 6723	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
|- F/_ y ( x e. A , y e. B |-> C )
Theorem	nfmpt2 6724*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
|- F/_ z A   &    |- F/_ z B   &    |- F/_ z C   =>    |- F/_ z ( x e. A , y e. B |-> C )
Theorem	mpt20 6725	A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
|- ( x e. (/) , y e. B |-> C ) = (/)
Theorem	oprab4 6726*	Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
|- { <. <. x , y >. , z >. | ( <. x , y >. e. ( A X. B ) /\ ph ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }
Theorem	cbvoprab1 6727*	Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.)
|- F/ w ph   &    |- F/ x ps   &    |- ( x = w -> ( ph <-> ps ) )   =>    |- { <. <. x , y >. , z >. | ph } = { <. <. w , y >. , z >. | ps }
Theorem	cbvoprab2 6728*	Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/ w ph   &    |- F/ y ps   &    |- ( y = w -> ( ph <-> ps ) )   =>    |- { <. <. x , y >. , z >. | ph } = { <. <. x , w >. , z >. | ps }
Theorem	cbvoprab12 6729*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- F/ w ph   &    |- F/ v ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = w /\ y = v ) -> ( ph <-> ps ) )   =>    |- { <. <. x , y >. , z >. | ph } = { <. <. w , v >. , z >. | ps }
Theorem	cbvoprab12v 6730*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
|- ( ( x = w /\ y = v ) -> ( ph <-> ps ) )   =>    |- { <. <. x , y >. , z >. | ph } = { <. <. w , v >. , z >. | ps }
Theorem	cbvoprab3 6731*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
|- F/ w ph   &    |- F/ z ps   &    |- ( z = w -> ( ph <-> ps ) )   =>    |- { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , w >. | ps }
Theorem	cbvoprab3v 6732*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( z = w -> ( ph <-> ps ) )   =>    |- { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , w >. | ps }
Theorem	cbvmpt2x 6733*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 6734 allows B to be a function of x. (Contributed by NM, 29-Dec-2014.)
|- F/_ z B   &    |- F/_ x D   &    |- F/_ z C   &    |- F/_ w C   &    |- F/_ x E   &    |- F/_ y E   &    |- ( x = z -> B = D )   &    |- ( ( x = z /\ y = w ) -> C = E )   =>    |- ( x e. A , y e. B |-> C ) = ( z e. A , w e. D |-> E )
Theorem	cbvmpt2 6734*	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	cbvmpt2v 6735*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4749, 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	elimdelov 6736	Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). (Contributed by Paul Chapman, 25-Mar-2008.)
|- ( ph -> C e. ( A F B ) )   &    |- Z e. ( X F Y )   =>    |- if ( ph , C , Z ) e. ( if ( ph , A , X ) F if ( ph , B , Y ) )
Theorem	ovif 6737	Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( if ( ph , A , B ) F C ) = if ( ph , ( A F C ) , ( B F C ) )
Theorem	ovif2 6738	Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 1-Oct-2018.)
|- ( A F if ( ph , B , C ) ) = if ( ph , ( A F B ) , ( A F C ) )
Theorem	ovif12 6739	Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( if ( ph , A , B ) F if ( ph , C , D ) ) = if ( ph , ( A F C ) , ( B F D ) )
Theorem	ifov 6740	Move a conditional outside of an operation. (Contributed by AV, 11-Nov-2019.)
|- ( A if ( ph , F , G ) B ) = if ( ph , ( A F B ) , ( A G B ) )
Theorem	dmoprab 6741*	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 6742*	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 6743*	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 6744*	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 6745*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
|- Rel dom { <. <. x , y >. , z >. | ph }
Theorem	oprabss 6746*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
|- { <. <. x , y >. , z >. | ph } C_ ( ( _V X. _V ) X. _V )
Theorem	eloprabga 6747*	The law of concretion for operation class abstraction. Compare elopab 4983. (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 6748*	The law of concretion for operation class abstraction. Compare elopab 4983. (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 6749*	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	mpt2v 6750*	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	mpt2mptx 6751*	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	mpt2mpt 6752*	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	mpt2difsnif 6753	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	mpt2snif 6754	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	fconstmpt2 6755*	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 6756*	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 6757*	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	resmpt2 6758*	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 6759*	"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 6760*	"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 6761*	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	mpt2fun 6762*	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 6763*	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 6764*	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 6765	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 6766*	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 6767*	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	fnov 6768*	Representation of a function in terms of its values. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( F Fn ( A X. B ) <-> F = ( x e. A , y e. B |-> ( x F y ) ) )
Theorem	mpt22eqb 6769*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 6767. (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	rnmpt2 6770*	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	reldmmpt2 6771*	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	elrnmpt2g 6772*	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	elrnmpt2 6773*	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	elrnmpt2res 6774*	Membership in the range of a restricted operation class abstraction. (Contributed by Thierry Arnoux, 25-May-2019.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( D e. V -> ( D e. ran ( F |` R ) <-> E. x e. A E. y e. B ( D = C /\ x R y ) ) )
Theorem	ralrnmpt2 6775*	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	rexrnmpt2 6776*	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 6777*	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 6778*	The value of an operation class abstraction. Compare ovidi 6779. 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 6779*	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 6780*	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 6781*	The value of an operation class abstraction. Compare ovig 6782. 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 6782*	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 6783*	Value of a function given by the "maps to" notation. (This is the operation analogue of fvmpt2 6291.) (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	ovmpt2s 6784*	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 6785*	The value of an operation class abstraction. A version of ovmpt2g 6795 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	ovmpt2dxf 6786*	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	ovmpt2dx 6787*	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	ovmpt2d 6788*	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	ovmpt2x 6789*	The value of an operation class abstraction. Variant of ovmpt2ga 6790 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	ovmpt2ga 6790*	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	ovmpt2a 6791*	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	ovmpt2df 6792*	Alternate deduction version of ovmpt2 6796, 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	ovmpt2dv 6793*	Alternate deduction version of ovmpt2 6796, 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	ovmpt2dv2 6794*	Alternate deduction version of ovmpt2 6796, 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	ovmpt2g 6795*	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	ovmpt2 6796*	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	ov3 6797*	The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
|- S e. _V   &    |- ( ( ( 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 6798*	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 6799*	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 6800	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 ) )