P. 61 of Theorem List - Intuitionistic Logic Explorer

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

Type	Label	Description
Statement
Theorem	acexmidlemab 6001*	Lemma for acexmid 6006. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) -> -. ph )
Theorem	acexmidlemcase 6002*	Lemma for acexmid 6006. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle). The cases are (1) the choice function evaluated at A equals { (/) }, (2) the choice function evaluated at B equals (/), and (3) the choice function evaluated at A equals (/) and the choice function evaluated at B equals { (/) }. Because of the way we represent the choice function y, the choice function evaluated at A is ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) and the choice function evaluated at B is ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ). Other than the difference in notation these work just as ( y ` A ) and ( y ` B ) would if y were a function as defined by df-fun 5320. Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at A equals { (/) }, then { (/) } e. A and likewise for B. (Contributed by Jim Kingdon, 7-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( { (/) } e. A \/ (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) )
Theorem	acexmidlem1 6003*	Lemma for acexmid 6006. List the cases identified in acexmidlemcase 6002 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ph \/ -. ph ) )
Theorem	acexmidlem2 6004*	Lemma for acexmid 6006. This builds on acexmidlem1 6003 by noting that every element of C is inhabited. (Note that y is not quite a function in the df-fun 5320 sense because it uses ordered pairs as described in opthreg 4648 rather than df-op 3675). The set A is also found in onsucelsucexmidlem 4621. (Contributed by Jim Kingdon, 5-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( A. z e. C A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ph \/ -. ph ) )
Theorem	acexmidlemv 6005*	Lemma for acexmid 6006. This is acexmid 6006 with additional disjoint variable conditions, most notably between ph and x. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )   =>    |- ( ph \/ -. ph )
Theorem	acexmid 6006*	The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer] p. 483. The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function y provides a value when z is inhabited (as opposed to nonempty as in some statements of the axiom of choice). Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967). For this theorem stated using the df-ac 7399 and df-exmid 4279 syntaxes, see exmidac 7402. (Contributed by Jim Kingdon, 4-Aug-2019.)
|- E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )   =>    |- ( ph \/ -. ph )
2.6.11  Operations
Syntax	co 6007	Extend class notation to include the value of an operation F (such as + ) for two arguments A and B. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous.
class ( A F B )
Syntax	coprab 6008	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class { <. <. x , y >. , z >. | ph }
Syntax	cmpo 6009	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 6010	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 6044 and ovprc2 6045. 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 6011. (Contributed by NM, 28-Feb-1995.)
|- ( A F B ) = ( F ` <. A , B >. )
Definition	df-oprab 6011*	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 6010 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 6146. (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 6012*	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 4147 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 6013	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( F = G -> ( A F B ) = ( A G B ) )
Theorem	oveq1 6014	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( A F C ) = ( B F C ) )
Theorem	oveq2 6015	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( C F A ) = ( C F B ) )
Theorem	oveq12 6016	Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
|- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
Theorem	oveq1i 6017	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( A F C ) = ( B F C )
Theorem	oveq2i 6018	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( C F A ) = ( C F B )
Theorem	oveq12i 6019	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 6020	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
|- A = B   =>    |- ( C A D ) = ( C B D )
Theorem	oveq123i 6021	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 6022	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A F C ) = ( B F C ) )
Theorem	oveq2d 6023	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C F A ) = ( C F B ) )
Theorem	oveqd 6024	Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C A D ) = ( C B D ) )
Theorem	oveq12d 6025	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 6026	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 6027	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 6028	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 6029	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 6030	Equality theorem for nested function and operation value. Closed form of fvoveq1d 6029. (Contributed by AV, 23-Jul-2022.)
|- ( A = B -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )
Theorem	ovanraleqv 6031*	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 6032	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 6033*	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 6034*	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 6035	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 6036	Deduction version of bound-variable hypothesis builder nfov 6037. (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 6037	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 6038*	Slight elaboration of exdistrfor 1846. A lemma for oprabid 6039. (Contributed by Jim Kingdon, 15-Jan-2019.)
|- ( E. x E. y ( x = z /\ ps ) -> E. x ( x = z /\ E. y ps ) )
Theorem	oprabid 6039	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 6040	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 6041	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 6042	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 6043	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 6044	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 6045	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 6046	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 6047*	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 6048*	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 6049*	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 6050*	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 6051	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 6052	Value of a binary operation expressed as a binary relation. See also fnbrfvb 5674 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 6053	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5675. (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 6054*	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 6055	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 6056*	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 6057*	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 6058*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
|- Rel { <. <. x , y >. , z >. | ph }
Theorem	nfoprab1 6059	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 6060	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 6061	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 6062*	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 6063*	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 6064*	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 6065*	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 6066	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4364. (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 6067	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4365. (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 6068	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4368. (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 6069*	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 6070*	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 6071*	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 6072*	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 6073	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 6074*	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 6075	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 6076*	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 6077	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 6078	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 6079*	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 6080	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 6081*	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 6082*	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 6083*	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 6084*	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 6085*	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 6086*	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 6087*	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 6088*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 6089 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 6089*	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 6090*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4179, 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 6091*	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 6092*	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 6093*	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 6094*	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 6095*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
|- Rel dom { <. <. x , y >. , z >. | ph }
Theorem	oprabss 6096*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
|- { <. <. x , y >. , z >. | ph } C_ ( ( _V X. _V ) X. _V )
Theorem	eloprabga 6097*	The law of concretion for operation class abstraction. Compare elopab 4346. (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 6098*	The law of concretion for operation class abstraction. Compare elopab 4346. (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 6099*	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 6100*	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 }