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
Syntax	coprab 6001	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class { <. <. x , y >. , z >. | ph }
Syntax	cmpo 6002	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class ( x e. A , y e. B |-> C )
Definition	df-ov 6003	Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation F and its arguments A and B- will be useful for proving meaningful theorems. For example, if class F is the operation + and arguments A and B are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets); see ovprc1 6037 and ovprc2 6038. On the other hand, we often find uses for this definition when F is a proper class. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6004. (Contributed by NM, 28-Feb-1995.)
|- ( A F B ) = ( F ` <. A , B >. )
Definition	df-oprab 6004*	Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally x, y, and z are distinct, although the definition doesn't strictly require it. See df-ov 6003 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpo 6139. (Contributed by NM, 12-Mar-1995.)
|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
Definition	df-mpo 6005*	Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x , y (in A X. B) to B ( x , y )". An extension of df-mpt 4146 for two arguments. (Contributed by NM, 17-Feb-2008.)
|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
Theorem	oveq 6006	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( F = G -> ( A F B ) = ( A G B ) )
Theorem	oveq1 6007	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( A F C ) = ( B F C ) )
Theorem	oveq2 6008	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( C F A ) = ( C F B ) )
Theorem	oveq12 6009	Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
|- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
Theorem	oveq1i 6010	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( A F C ) = ( B F C )
Theorem	oveq2i 6011	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( C F A ) = ( C F B )
Theorem	oveq12i 6012	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- A = B   &    |- C = D   =>    |- ( A F C ) = ( B F D )
Theorem	oveqi 6013	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
|- A = B   =>    |- ( C A D ) = ( C B D )
Theorem	oveq123i 6014	Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
|- A = C   &    |- B = D   &    |- F = G   =>    |- ( A F B ) = ( C G D )
Theorem	oveq1d 6015	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A F C ) = ( B F C ) )
Theorem	oveq2d 6016	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C F A ) = ( C F B ) )
Theorem	oveqd 6017	Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C A D ) = ( C B D ) )
Theorem	oveq12d 6018	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A F C ) = ( B F D ) )
Theorem	oveqan12d 6019	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ph /\ ps ) -> ( A F C ) = ( B F D ) )
Theorem	oveqan12rd 6020	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ps /\ ph ) -> ( A F C ) = ( B F D ) )
Theorem	oveq123d 6021	Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
|- ( ph -> F = G )   &    |- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A F C ) = ( B G D ) )
Theorem	fvoveq1d 6022	Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.)
|- ( ph -> A = B )   =>    |- ( ph -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )
Theorem	fvoveq1 6023	Equality theorem for nested function and operation value. Closed form of fvoveq1d 6022. (Contributed by AV, 23-Jul-2022.)
|- ( A = B -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )
Theorem	ovanraleqv 6024*	Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.)
|- ( B = X -> ( ph <-> ps ) )   =>    |- ( B = X -> ( A. x e. V ( ph /\ ( A .x. B ) = C ) <-> A. x e. V ( ps /\ ( A .x. X ) = C ) ) )
Theorem	imbrov2fvoveq 6025	Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.)
|- ( X = Y -> ( ph <-> ps ) )   =>    |- ( X = Y -> ( ( ph -> ( F ` ( ( G ` X ) .x. O ) ) R A ) <-> ( ps -> ( F ` ( ( G ` Y ) .x. O ) ) R A ) ) )
Theorem	ovrspc2v 6026*	If an operation value is element of a class for all operands of two classes, then the operation value is an element of the class for specific operands of the two classes. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- ( ( ( X e. A /\ Y e. B ) /\ A. x e. A A. y e. B ( x F y ) e. C ) -> ( X F Y ) e. C )
Theorem	oveqrspc2v 6027*	Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x F y ) = ( x G y ) )   =>    |- ( ( ph /\ ( X e. A /\ Y e. B ) ) -> ( X F Y ) = ( X G Y ) )
Theorem	oveqdr 6028	Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)
|- ( ph -> F = G )   =>    |- ( ( ph /\ ps ) -> ( x F y ) = ( x G y ) )
Theorem	nfovd 6029	Deduction version of bound-variable hypothesis builder nfov 6030. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x F )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x ( A F B ) )
Theorem	nfov 6030	Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
|- F/_ x A   &    |- F/_ x F   &    |- F/_ x B   =>    |- F/_ x ( A F B )
Theorem	oprabidlem 6031*	Slight elaboration of exdistrfor 1846. A lemma for oprabid 6032. (Contributed by Jim Kingdon, 15-Jan-2019.)
|- ( E. x E. y ( x = z /\ ps ) -> E. x ( x = z /\ E. y ps ) )
Theorem	oprabid 6032	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Although this theorem would be useful with a distinct variable condition between x, y, and z, we use ax-bndl 1555 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)
|- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )
Theorem	fnovex 6033	The result of an operation is a set. (Contributed by Jim Kingdon, 15-Jan-2019.)
|- ( ( F Fn ( C X. D ) /\ A e. C /\ B e. D ) -> ( A F B ) e. _V )
Theorem	ovexg 6034	Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.)
|- ( ( A e. V /\ F e. W /\ B e. X ) -> ( A F B ) e. _V )
Theorem	ovssunirng 6035	The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- ( ( X e. V /\ Y e. W ) -> ( X F Y ) C_ U. ran F )
Theorem	ovprc 6036	The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- Rel dom F   =>    |- ( -. ( A e. _V /\ B e. _V ) -> ( A F B ) = (/) )
Theorem	ovprc1 6037	The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)
|- Rel dom F   =>    |- ( -. A e. _V -> ( A F B ) = (/) )
Theorem	ovprc2 6038	The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- Rel dom F   =>    |- ( -. B e. _V -> ( A F B ) = (/) )
Theorem	csbov123g 6039	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- ( A e. D -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) )
Theorem	csbov12g 6040*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B F [_ A / x ]_ C ) )
Theorem	csbov1g 6041*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B F C ) )
Theorem	csbov2g 6042*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( B F [_ A / x ]_ C ) )
Theorem	rspceov 6043*	A frequently used special case of rspc2ev 2922 for operation values. (Contributed by NM, 21-Mar-2007.)
|- ( ( C e. A /\ D e. B /\ S = ( C F D ) ) -> E. x e. A E. y e. B S = ( x F y ) )
Theorem	elovimad 6044	Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. D )   &    |- ( ph -> Fun F )   &    |- ( ph -> ( C X. D ) C_ dom F )   =>    |- ( ph -> ( A F B ) e. ( F " ( C X. D ) ) )
Theorem	fnbrovb 6045	Value of a binary operation expressed as a binary relation. See also fnbrfvb 5671 for functions on Cartesian products. (Contributed by BJ, 15-Feb-2022.)
|- ( ( F Fn ( V X. W ) /\ ( A e. V /\ B e. W ) ) -> ( ( A F B ) = C <-> <. A , B >. F C ) )
Theorem	fnotovb 6046	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5672. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( ( C F D ) = R <-> <. C , D , R >. e. F ) )
Theorem	opabbrex 6047*	A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
|- ( ( V e. _V /\ E e. _V ) -> ( f ( V W E ) p -> th ) )   &    |- ( ( V e. _V /\ E e. _V ) -> { <. f , p >. | th } e. _V )   =>    |- ( ( V e. _V /\ E e. _V ) -> { <. f , p >. | ( f ( V W E ) p /\ ps ) } e. _V )
Theorem	0neqopab 6048	The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
|- -. (/) e. { <. x , y >. | ph }
Theorem	brabvv 6049*	If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Jim Kingdon, 16-Jan-2019.)
|- ( X { <. x , y >. | ph } Y -> ( X e. _V /\ Y e. _V ) )
Theorem	dfoprab2 6050*	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 6051*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
|- Rel { <. <. x , y >. , z >. | ph }
Theorem	nfoprab1 6052	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 6053	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 6054	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 6055*	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 6056*	Equivalent wff's yield equal operation class abstractions (deduction form). (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 6057*	Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. <. x , y >. , z >. | ps } = { <. <. x , y >. , z >. | ch } )
Theorem	oprabbii 6058*	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 6059	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4363. (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 6060	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4364. (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 6061	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4367. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , z >. | ps } <-> A. x A. y A. z ( ph <-> ps ) )
Theorem	mpoeq123 6062*	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	mpoeq12 6063*	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	mpoeq123dva 6064*	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	mpoeq123dv 6065*	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	mpoeq123i 6066	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	mpoeq3dva 6067*	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	mpoeq3ia 6068	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	mpoeq3dv 6069*	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	nfmpo1 6070	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	nfmpo2 6071	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	nfmpo 6072*	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	mpo0 6073	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 6074*	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 6075*	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 6076*	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 6077*	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 6078*	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 6079*	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 6080*	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	cbvmpox 6081*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 6082 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	cbvmpo 6082*	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 6083*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4178, 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 6084*	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 6085*	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 6086*	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 6087*	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 6088*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
|- Rel dom { <. <. x , y >. , z >. | ph }
Theorem	oprabss 6089*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
|- { <. <. x , y >. , z >. | ph } C_ ( ( _V X. _V ) X. _V )
Theorem	eloprabga 6090*	The law of concretion for operation class abstraction. Compare elopab 4345. (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 6091*	The law of concretion for operation class abstraction. Compare elopab 4345. (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 6092*	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 6093*	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 6094*	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 6095*	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 6096	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 6097	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 6098*	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 6099*	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 6100*	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 ) } )