P. 61 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isoeq4 6001	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
|- ( A = C -> ( H Isom R , S ( A , B ) <-> H Isom R , S ( C , B ) ) )
Theorem	isoeq5 6002	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
|- ( B = C -> ( H Isom R , S ( A , B ) <-> H Isom R , S ( A , C ) ) )
Theorem	nfiso 6003	Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- F/_ x H   &    |- F/_ x R   &    |- F/_ x S   &    |- F/_ x A   &    |- F/_ x B   =>    |- F/ x H Isom R , S ( A , B )
Theorem	isof1o 6004	An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
|- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
Theorem	isorel 6005	An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
|- ( ( H Isom R , S ( A , B ) /\ ( C e. A /\ D e. A ) ) -> ( C R D <-> ( H ` C ) S ( H ` D ) ) )
Theorem	soisores 6006*	Express the condition of isomorphism on two strict orders for a function's restriction. (Contributed by Mario Carneiro, 22-Jan-2015.)
|- ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) ) -> ( ( F |` A ) Isom R , S ( A , ( F " A ) ) <-> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) )
Theorem	soisoi 6007*	Infer isomorphism from one direction of an order proof for isomorphisms between strict orders. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> H Isom R , S ( A , B ) )
Theorem	isoid 6008	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
|- ( _I |` A ) Isom R , R ( A , A )
Theorem	isocnv 6009	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
|- ( H Isom R , S ( A , B ) -> `' H Isom S , R ( B , A ) )
Theorem	isocnv2 6010	Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
|- ( H Isom R , S ( A , B ) <-> H Isom `' R , `' S ( A , B ) )
Theorem	isocnv3 6011	Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- C = ( ( A X. A ) \ R )   &    |- D = ( ( B X. B ) \ S )   =>    |- ( H Isom R , S ( A , B ) <-> H Isom C , D ( A , B ) )
Theorem	isores2 6012	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
|- ( H Isom R , S ( A , B ) <-> H Isom R , ( S i^i ( B X. B ) ) ( A , B ) )
Theorem	isores1 6013	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
|- ( H Isom R , S ( A , B ) <-> H Isom ( R i^i ( A X. A ) ) , S ( A , B ) )
Theorem	isores3 6014	Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
|- ( ( H Isom R , S ( A , B ) /\ K C_ A /\ X = ( H " K ) ) -> ( H |` K ) Isom R , S ( K , X ) )
Theorem	isotr 6015	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- ( ( H Isom R , S ( A , B ) /\ G Isom S , T ( B , C ) ) -> ( G o. H ) Isom R , T ( A , C ) )
Theorem	isomin 6016	Isomorphisms preserve minimal elements. Note that ( `' R " { D } ) is Takeuti and Zaring's idiom for the initial segment { x | x R D }. Proposition 6.31(1) of [TakeutiZaring] p. 33. (Contributed by NM, 19-Apr-2004.)
|- ( ( H Isom R , S ( A , B ) /\ ( C C_ A /\ D e. A ) ) -> ( ( C i^i ( `' R " { D } ) ) = (/) <-> ( ( H " C ) i^i ( `' S " { ( H ` D ) } ) ) = (/) ) )
Theorem	isoini 6017	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
|- ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( H " ( A i^i ( `' R " { D } ) ) ) = ( B i^i ( `' S " { ( H ` D ) } ) ) )
Theorem	isoini2 6018	Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
|- C = ( A i^i ( `' R " { X } ) )   &    |- D = ( B i^i ( `' S " { ( H ` X ) } ) )   =>    |- ( ( H Isom R , S ( A , B ) /\ X e. A ) -> ( H |` C ) Isom R , S ( C , D ) )
Theorem	isofrlem 6019*	Lemma for isofr 6021. (Contributed by NM, 29-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
|- ( ph -> H Isom R , S ( A , B ) )   &    |- ( ph -> ( H " x ) e. _V )   =>    |- ( ph -> ( S Fr B -> R Fr A ) )
Theorem	isoselem 6020*	Lemma for isose 6022. (Contributed by Mario Carneiro, 23-Jun-2015.)
|- ( ph -> H Isom R , S ( A , B ) )   &    |- ( ph -> ( H " x ) e. _V )   =>    |- ( ph -> ( R Se A -> S Se B ) )
Theorem	isofr 6021	An isomorphism preserves well-foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( R Fr A <-> S Fr B ) )
Theorem	isose 6022	An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.)
|- ( H Isom R , S ( A , B ) -> ( R Se A <-> S Se B ) )
Theorem	isofr2 6023	A weak form of isofr 6021 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.)
|- ( ( H Isom R , S ( A , B ) /\ B e. V ) -> ( S Fr B -> R Fr A ) )
Theorem	isopolem 6024	Lemma for isopo 6025. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( S Po B -> R Po A ) )
Theorem	isopo 6025	An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( R Po A <-> S Po B ) )
Theorem	isosolem 6026	Lemma for isoso 6027. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( S Or B -> R Or A ) )
Theorem	isoso 6027	An isomorphism preserves strict ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( R Or A <-> S Or B ) )
Theorem	isowe 6028	An isomorphism preserves well-ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( R We A <-> S We B ) )
Theorem	isowe2 6029*	A weak form of isowe 6028 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.)
|- ( ( H Isom R , S ( A , B ) /\ A. x ( H " x ) e. _V ) -> ( S We B -> R We A ) )
Theorem	f1oiso 6030*	Any one-to-one onto function determines an isomorphism with an induced relation S. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.)
|- ( ( H : A -1-1-onto-> B /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) -> H Isom R , S ( A , B ) )
Theorem	f1oiso2 6031*	Any one-to-one onto function determines an isomorphism with an induced relation S. (Contributed by Mario Carneiro, 9-Mar-2013.)
|- S = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) }   =>    |- ( H : A -1-1-onto-> B -> H Isom R , S ( A , B ) )
Theorem	f1owe 6032*	Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997.)
|- R = { <. x , y >. | ( F ` x ) S ( F ` y ) }   =>    |- ( F : A -1-1-onto-> B -> ( S We B -> R We A ) )
Theorem	f1oweALT 6033*	Well-ordering of isomorphic relations. (This version is proved directly instead of with the isomorphism predicate.) (Contributed by NM, 4-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.)
|- R = { <. x , y >. | ( F ` x ) S ( F ` y ) }   =>    |- ( F : A -1-1-onto-> B -> ( S We B -> R We A ) )
Theorem	weniso 6034	A set-like well-ordering has no nontrivial automorphisms. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)
|- ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> F = ( _I |` A ) )
Theorem	weisoeq 6035	Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso 6037. (Contributed by Mario Carneiro, 25-Jun-2015.)
|- ( ( ( R We A /\ R Se A ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> F = G )
Theorem	weisoeq2 6036	Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso2 6038. (Contributed by Mario Carneiro, 25-Jun-2015.)
|- ( ( ( S We B /\ S Se B ) /\ ( F Isom R , S ( A , B ) /\ G Isom R , S ( A , B ) ) ) -> F = G )
Theorem	wemoiso 6037*	Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu 7950. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
|- ( R We A -> E* f f Isom R , S ( A , B ) )
Theorem	wemoiso2 6038*	Thus, there is at most one isomorphism between any two well-ordered sets. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
|- ( S We B -> E* f f Isom R , S ( A , B ) )
Theorem	knatar 6039*	The Knaster-Tarski theorem says that every monotone function over a complete lattice has a (least) fixpoint. Here we specialize this theorem to the case when the lattice is the powerset lattice ~P A. (Contributed by Mario Carneiro, 11-Jun-2015.)
|- X = |^| { z e. ~P A | ( F ` z ) C_ z }   =>    |- ( ( A e. V /\ ( F ` A ) C_ A /\ A. x e. ~P A A. y e. ~P x ( F ` y ) C_ ( F ` x ) ) -> ( X C_ A /\ ( F ` X ) = X ) )
2.4.10  Operations
Syntax	co 6040	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. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 9248.)
class ( A F B )
Syntax	coprab 6041	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class { <. <. x , y >. , z >. | ph }
Syntax	cmpt2 6042	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 6043	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 (see 3p2e5 10067). 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 6068 and ovprc2 6069. On the other hand, we often find uses for this definition when F is a proper class, such as +o in oav 6714. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6044. (Contributed by NM, 28-Feb-1995.)
|- ( A F B ) = ( F ` <. A , B >. )
Definition	df-oprab 6044*	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 6043 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 ovmpt2 6168. (Contributed by NM, 12-Mar-1995.)
|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
Definition	df-mpt2 6045*	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 4228 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 6046	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( F = G -> ( A F B ) = ( A G B ) )
Theorem	oveq1 6047	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( A F C ) = ( B F C ) )
Theorem	oveq2 6048	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( C F A ) = ( C F B ) )
Theorem	oveq12 6049	Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
|- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
Theorem	oveq1i 6050	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( A F C ) = ( B F C )
Theorem	oveq2i 6051	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( C F A ) = ( C F B )
Theorem	oveq12i 6052	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 6053	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
|- A = B   =>    |- ( C A D ) = ( C B D )
Theorem	oveq123i 6054	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 6055	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A F C ) = ( B F C ) )
Theorem	oveq2d 6056	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C F A ) = ( C F B ) )
Theorem	oveqd 6057	Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C A D ) = ( C B D ) )
Theorem	oveq12d 6058	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 6059	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 6060	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 6061	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	nfovd 6062	Deduction version of bound-variable hypothesis builder nfov 6063. (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 6063	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	oprabid 6064	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 20-Mar-2013.)
|- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )
Theorem	ovex 6065	The result of an operation is a set. (Contributed by NM, 13-Mar-1995.)
|- ( A F B ) e. _V
Theorem	ovssunirn 6066	The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- ( X F Y ) C_ U. ran F
Theorem	ovprc 6067	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 6068	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 6069	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	ovrcl 6070	Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015.)
|- Rel dom F   =>    |- ( C e. ( A F B ) -> ( A e. _V /\ B e. _V ) )
Theorem	csbovg 6071	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 6072*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- ( A e. D -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B F [_ A / x ]_ C ) )
Theorem	csbov1g 6073*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- ( A e. D -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B F C ) )
Theorem	csbov2g 6074*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- ( A e. D -> [_ A / x ]_ ( B F C ) = ( B F [_ A / x ]_ C ) )
Theorem	rspceov 6075*	A frequently used special case of rspc2ev 3020 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	fnotovb 6076	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5727. (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 6077*	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 6078	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	brabv 6079	If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
|- ( X { <. x , y >. | ph } Y -> ( X e. _V /\ Y e. _V ) )
Theorem	dfoprab2 6080*	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 6081*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
|- Rel { <. <. x , y >. , z >. | ph }
Theorem	nfoprab1 6082	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 6083	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 6084	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 6085*	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 6086*	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 6087*	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 6088*	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 6089	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4440. (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 6090	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4441. (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 6091	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4444. (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 6092*	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 6093*	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 6094*	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 6095*	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 6096	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 6097*	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 6098	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	nfmpt21 6099	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 6100	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 )