P. 63 of Theorem List - Intuitionistic Logic Explorer

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

Type	Label	Description
Statement
Theorem	abexex 6201*	A condition where a class builder continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007.)
|- A e. _V   &    |- ( ph -> x e. A )   &    |- { y | ph } e. _V   =>    |- { y | E. x ph } e. _V
Theorem	oprabexd 6202*	Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> E* z ps )   &    |- ( ph -> F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } )   =>    |- ( ph -> F e. _V )
Theorem	oprabex 6203*	Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.)
|- A e. _V   &    |- B e. _V   &    |- ( ( x e. A /\ y e. B ) -> E* z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }   =>    |- F e. _V
Theorem	oprabex3 6204*	Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.)
|- H e. _V   &    |- 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 ) ) }   =>    |- F e. _V
Theorem	oprabrexex2 6205*	Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.)
|- A e. _V   &    |- { <. <. x , y >. , z >. | ph } e. _V   =>    |- { <. <. x , y >. , z >. | E. w e. A ph } e. _V
Theorem	ab2rexex 6206*	Existence of a class abstraction of existentially restricted sets. Variables x and y are normally free-variable parameters in the class expression substituted for C, which can be thought of as C ( x , y ). See comments for abrexex 6192. (Contributed by NM, 20-Sep-2011.)
|- A e. _V   &    |- B e. _V   =>    |- { z | E. x e. A E. y e. B z = C } e. _V
Theorem	ab2rexex2 6207*	Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x, y, and z. Compare abrexex2 6199. (Contributed by NM, 20-Sep-2011.)
|- A e. _V   &    |- B e. _V   &    |- { z | ph } e. _V   =>    |- { z | E. x e. A E. y e. B ph } e. _V
Theorem	xpexgALT 6208	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. This version is proven using Replacement; see xpexg 4787 for a version that uses the Power Set axiom instead. (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
Theorem	offval3 6209*	General value of ( F oF R G ) with no assumptions on functionality of F and G. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( ( F e. V /\ G e. W ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )
Theorem	offres 6210	Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( ( F e. V /\ G e. W ) -> ( ( F oF R G ) |` D ) = ( ( F |` D ) oF R ( G |` D ) ) )
Theorem	ofmres 6211*	Equivalent expressions for a restriction of the function operation map. Unlike oF R which is a proper class, ( oF R |` ( A X. B ) ) can be a set by ofmresex 6212, allowing it to be used as a function or structure argument. By ofmresval 6160, the restricted operation map values are the same as the original values, allowing theorems for oF R to be reused. (Contributed by NM, 20-Oct-2014.)
|- ( oF R |` ( A X. B ) ) = ( f e. A , g e. B |-> ( f oF R g ) )
Theorem	ofmresex 6212	Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( oF R |` ( A X. B ) ) e. _V )
Theorem	uchoice 6213*	Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7301 (with the key difference being the change of E. to E!) but unique choice in fact follows from the axiom of collection and our other axioms. This is somewhat similar to Corollary 3.9.2 of [HoTT], p. (varies) but is better described by the paragraph at the end of Section 3.9 which starts "A similar issue arises in set-theoretic mathematics". (Contributed by Jim Kingdon, 13-Sep-2025.)
|- ( ( A e. V /\ A. x e. A E! y ph ) -> E. f ( f Fn A /\ A. x e. A [. ( f ` x ) / y ]. ph ) )
2.6.15  First and second members of an ordered pair
Syntax	c1st 6214	Extend the definition of a class to include the first member an ordered pair function.
class 1st
Syntax	c2nd 6215	Extend the definition of a class to include the second member an ordered pair function.
class 2nd
Definition	df-1st 6216	Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 6222 proves that it does this. For example, ( 1st ` <. 3 , 4 >.) = 3 . Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 5161 and op1stb 4523). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 1st = ( x e. _V |-> U. dom { x } )
Definition	df-2nd 6217	Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 6223 proves that it does this. For example, ( 2nd ` <. 3 , 4 >.) = 4 . Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 5164 and op2ndb 5163). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 2nd = ( x e. _V |-> U. ran { x } )
Theorem	1stvalg 6218	The value of the function that extracts the first member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. _V -> ( 1st ` A ) = U. dom { A } )
Theorem	2ndvalg 6219	The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. _V -> ( 2nd ` A ) = U. ran { A } )
Theorem	1st0 6220	The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 1st ` (/) ) = (/)
Theorem	2nd0 6221	The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 2nd ` (/) ) = (/)
Theorem	op1st 6222	Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
|- A e. _V   &    |- B e. _V   =>    |- ( 1st ` <. A , B >. ) = A
Theorem	op2nd 6223	Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
|- A e. _V   &    |- B e. _V   =>    |- ( 2nd ` <. A , B >. ) = B
Theorem	op1std 6224	Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( C = <. A , B >. -> ( 1st ` C ) = A )
Theorem	op2ndd 6225	Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( C = <. A , B >. -> ( 2nd ` C ) = B )
Theorem	op1stg 6226	Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
|- ( ( A e. V /\ B e. W ) -> ( 1st ` <. A , B >. ) = A )
Theorem	op2ndg 6227	Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
|- ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B )
Theorem	ot1stg 6228	Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg 6228, ot2ndg 6229, ot3rdgg 6230.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( 1st ` ( 1st ` <. A , B , C >. ) ) = A )
Theorem	ot2ndg 6229	Extract the second member of an ordered triple. (See ot1stg 6228 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( 2nd ` ( 1st ` <. A , B , C >. ) ) = B )
Theorem	ot3rdgg 6230	Extract the third member of an ordered triple. (See ot1stg 6228 comment.) (Contributed by NM, 3-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( 2nd ` <. A , B , C >. ) = C )
Theorem	1stval2 6231	Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
|- ( A e. ( _V X. _V ) -> ( 1st ` A ) = |^| |^| A )
Theorem	2ndval2 6232	Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
|- ( A e. ( _V X. _V ) -> ( 2nd ` A ) = |^| |^| |^| `' { A } )
Theorem	fo1st 6233	The 1st function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- 1st : _V -onto-> _V
Theorem	fo2nd 6234	The 2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- 2nd : _V -onto-> _V
Theorem	f1stres 6235	Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( 1st |` ( A X. B ) ) : ( A X. B ) --> A
Theorem	f2ndres 6236	Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( 2nd |` ( A X. B ) ) : ( A X. B ) --> B
Theorem	fo1stresm 6237*	Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|- ( E. y y e. B -> ( 1st |` ( A X. B ) ) : ( A X. B ) -onto-> A )
Theorem	fo2ndresm 6238*	Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|- ( E. x x e. A -> ( 2nd |` ( A X. B ) ) : ( A X. B ) -onto-> B )
Theorem	1stcof 6239	Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.)
|- ( F : A --> ( B X. C ) -> ( 1st o. F ) : A --> B )
Theorem	2ndcof 6240	Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.)
|- ( F : A --> ( B X. C ) -> ( 2nd o. F ) : A --> C )
Theorem	xp1st 6241	Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. ( B X. C ) -> ( 1st ` A ) e. B )
Theorem	xp2nd 6242	Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. ( B X. C ) -> ( 2nd ` A ) e. C )
Theorem	1stexg 6243	Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.)
|- ( A e. V -> ( 1st ` A ) e. _V )
Theorem	2ndexg 6244	Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.)
|- ( A e. V -> ( 2nd ` A ) e. _V )
Theorem	elxp6 6245	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp4 5167. (Contributed by NM, 9-Oct-2004.)
|- ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
Theorem	elxp7 6246	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp4 5167. (Contributed by NM, 19-Aug-2006.)
|- ( A e. ( B X. C ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
Theorem	oprssdmm 6247*	Domain of closure of an operation. (Contributed by Jim Kingdon, 23-Oct-2023.)
|- ( ( ph /\ u e. S ) -> E. v v e. u )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   &    |- ( ph -> Rel F )   =>    |- ( ph -> ( S X. S ) C_ dom F )
Theorem	eqopi 6248	Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.)
|- ( ( A e. ( V X. W ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) -> A = <. B , C >. )
Theorem	xp2 6249*	Representation of cross product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.)
|- ( A X. B ) = { x e. ( _V X. _V ) | ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. B ) }
Theorem	unielxp 6250	The membership relation for a cross product is inherited by union. (Contributed by NM, 16-Sep-2006.)
|- ( A e. ( B X. C ) -> U. A e. U. ( B X. C ) )
Theorem	1st2nd2 6251	Reconstruction of a member of a cross product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013.)
|- ( A e. ( B X. C ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
Theorem	xpopth 6252	An ordered pair theorem for members of cross products. (Contributed by NM, 20-Jun-2007.)
|- ( ( A e. ( C X. D ) /\ B e. ( R X. S ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> A = B ) )
Theorem	eqop 6253	Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
|- ( A e. ( V X. W ) -> ( A = <. B , C >. <-> ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) )
Theorem	eqop2 6254	Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.)
|- B e. _V   &    |- C e. _V   =>    |- ( A = <. B , C >. <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) )
Theorem	op1steq 6255*	Two ways of expressing that an element is the first member of an ordered pair. (Contributed by NM, 22-Sep-2013.) (Revised by Mario Carneiro, 23-Feb-2014.)
|- ( A e. ( V X. W ) -> ( ( 1st ` A ) = B <-> E. x A = <. B , x >. ) )
Theorem	2nd1st 6256	Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.)
|- ( A e. ( B X. C ) -> U. `' { A } = <. ( 2nd ` A ) , ( 1st ` A ) >. )
Theorem	1st2nd 6257	Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006.)
|- ( ( Rel B /\ A e. B ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
Theorem	1stdm 6258	The first ordered pair component of a member of a relation belongs to the domain of the relation. (Contributed by NM, 17-Sep-2006.)
|- ( ( Rel R /\ A e. R ) -> ( 1st ` A ) e. dom R )
Theorem	2ndrn 6259	The second ordered pair component of a member of a relation belongs to the range of the relation. (Contributed by NM, 17-Sep-2006.)
|- ( ( Rel R /\ A e. R ) -> ( 2nd ` A ) e. ran R )
Theorem	1st2ndbr 6260	Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.)
|- ( ( Rel B /\ A e. B ) -> ( 1st ` A ) B ( 2nd ` A ) )
Theorem	releldm2 6261*	Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013.)
|- ( Rel A -> ( B e. dom A <-> E. x e. A ( 1st ` x ) = B ) )
Theorem	reldm 6262*	An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013.)
|- ( Rel A -> dom A = ran ( x e. A |-> ( 1st ` x ) ) )
Theorem	sbcopeq1a 6263	Equality theorem for substitution of a class for an ordered pair (analog of sbceq1a 3007 that avoids the existential quantifiers of copsexg 4287). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( A = <. x , y >. -> ( [. ( 1st ` A ) / x ]. [. ( 2nd ` A ) / y ]. ph <-> ph ) )
Theorem	csbopeq1a 6264	Equality theorem for substitution of a class A for an ordered pair <. x , y >. in B (analog of csbeq1a 3101). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( A = <. x , y >. -> [_ ( 1st ` A ) / x ]_ [_ ( 2nd ` A ) / y ]_ B = B )
Theorem	dfopab2 6265*	A way to define an ordered-pair class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- { <. x , y >. | ph } = { z e. ( _V X. _V ) | [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph }
Theorem	dfoprab3s 6266*	A way to define an operation class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- { <. <. x , y >. , z >. | ph } = { <. w , z >. | ( w e. ( _V X. _V ) /\ [. ( 1st ` w ) / x ]. [. ( 2nd ` w ) / y ]. ph ) }
Theorem	dfoprab3 6267*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.)
|- ( w = <. x , y >. -> ( ph <-> ps ) )   =>    |- { <. w , z >. | ( w e. ( _V X. _V ) /\ ph ) } = { <. <. x , y >. , z >. | ps }
Theorem	dfoprab4 6268*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( w = <. x , y >. -> ( ph <-> ps ) )   =>    |- { <. w , z >. | ( w e. ( A X. B ) /\ ph ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) }
Theorem	dfoprab4f 6269*	Operation class abstraction expressed without existential quantifiers. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- F/ x ph   &    |- F/ y ph   &    |- ( w = <. x , y >. -> ( ph <-> ps ) )   =>    |- { <. w , z >. | ( w e. ( A X. B ) /\ ph ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) }
Theorem	dfxp3 6270*	Define the cross product of three classes. Compare df-xp 4679. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.)
|- ( ( A X. B ) X. C ) = { <. <. x , y >. , z >. | ( x e. A /\ y e. B /\ z e. C ) }
Theorem	elopabi 6271*	A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.)
|- ( x = ( 1st ` A ) -> ( ph <-> ps ) )   &    |- ( y = ( 2nd ` A ) -> ( ps <-> ch ) )   =>    |- ( A e. { <. x , y >. | ph } -> ch )
Theorem	eloprabi 6272*	A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( x = ( 1st ` ( 1st ` A ) ) -> ( ph <-> ps ) )   &    |- ( y = ( 2nd ` ( 1st ` A ) ) -> ( ps <-> ch ) )   &    |- ( z = ( 2nd ` A ) -> ( ch <-> th ) )   =>    |- ( A e. { <. <. x , y >. , z >. | ph } -> th )
Theorem	mpomptsx 6273*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( x e. A , y e. B |-> C ) = ( z e. U_ x e. A ( { x } X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )
Theorem	mpompts 6274*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.)
|- ( x e. A , y e. B |-> C ) = ( z e. ( A X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )
Theorem	dmmpossx 6275*	The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- dom F C_ U_ x e. A ( { x } X. B )
Theorem	fmpox 6276*	Functionality, domain and codomain of a class given by the maps-to notation, where B ( x ) is not constant but depends on x. (Contributed by NM, 29-Dec-2014.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( A. x e. A A. y e. B C e. D <-> F : U_ x e. A ( { x } X. B ) --> D )
Theorem	fmpo 6277*	Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( A. x e. A A. y e. B C e. D <-> F : ( A X. B ) --> D )
Theorem	fnmpo 6278*	Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( A. x e. A A. y e. B C e. V -> F Fn ( A X. B ) )
Theorem	fnmpoi 6279*	Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
|- F = ( x e. A , y e. B |-> C )   &    |- C e. _V   =>    |- F Fn ( A X. B )
Theorem	dmmpo 6280*	Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
|- F = ( x e. A , y e. B |-> C )   &    |- C e. _V   =>    |- dom F = ( A X. B )
Theorem	mpofvex 6281*	Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( A. x A. y C e. V /\ R e. W /\ S e. X ) -> ( R F S ) e. _V )
Theorem	mpofvexi 6282*	Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- F = ( x e. A , y e. B |-> C )   &    |- C e. _V   &    |- R e. _V   &    |- S e. _V   =>    |- ( R F S ) e. _V
Theorem	ovmpoelrn 6283*	An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.)
|- O = ( x e. A , y e. B |-> C )   =>    |- ( ( A. x e. A A. y e. B C e. M /\ X e. A /\ Y e. B ) -> ( X O Y ) e. M )
Theorem	dmmpoga 6284*	Domain of an operation given by the maps-to notation, closed form of dmmpo 6280. (Contributed by Alexander van der Vekens, 10-Feb-2019.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( A. x e. A A. y e. B C e. V -> dom F = ( A X. B ) )
Theorem	dmmpog 6285*	Domain of an operation given by the maps-to notation, closed form of dmmpo 6280. Caution: This theorem is only valid in the very special case where the value of the mapping is a constant! (Contributed by Alexander van der Vekens, 1-Jun-2017.) (Proof shortened by AV, 10-Feb-2019.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( C e. V -> dom F = ( A X. B ) )
Theorem	mpoexxg 6286*	Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( A e. R /\ A. x e. A B e. S ) -> F e. _V )
Theorem	mpoexg 6287*	Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( A e. R /\ B e. S ) -> F e. _V )
Theorem	mpoexga 6288*	If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by NM, 12-Sep-2011.)
|- ( ( A e. V /\ B e. W ) -> ( x e. A , y e. B |-> C ) e. _V )
Theorem	mpoexw 6289*	Weak version of mpoex 6290 that holds without ax-coll 4158. If the domain and codomain of an operation given by maps-to notation are sets, the operation is a set. (Contributed by Rohan Ridenour, 14-Aug-2023.)
|- A e. _V   &    |- B e. _V   &    |- D e. _V   &    |- A. x e. A A. y e. B C e. D   =>    |- ( x e. A , y e. B |-> C ) e. _V
Theorem	mpoex 6290*	If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013.)
|- A e. _V   &    |- B e. _V   =>    |- ( x e. A , y e. B |-> C ) e. _V
Theorem	fnmpoovd 6291*	A function with a Cartesian product as domain is a mapping with two arguments defined by its operation values. (Contributed by AV, 20-Feb-2019.) (Revised by AV, 3-Jul-2022.)
|- ( ph -> M Fn ( A X. B ) )   &    |- ( ( i = a /\ j = b ) -> D = C )   &    |- ( ( ph /\ i e. A /\ j e. B ) -> D e. U )   &    |- ( ( ph /\ a e. A /\ b e. B ) -> C e. V )   =>    |- ( ph -> ( M = ( a e. A , b e. B |-> C ) <-> A. i e. A A. j e. B ( i M j ) = D ) )
Theorem	fmpoco 6292*	Composition of two functions. Variation of fmptco 5740 when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> R e. C )   &    |- ( ph -> F = ( x e. A , y e. B |-> R ) )   &    |- ( ph -> G = ( z e. C |-> S ) )   &    |- ( z = R -> S = T )   =>    |- ( ph -> ( G o. F ) = ( x e. A , y e. B |-> T ) )
Theorem	oprabco 6293*	Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 26-Sep-2015.)
|- ( ( x e. A /\ y e. B ) -> C e. D )   &    |- F = ( x e. A , y e. B |-> C )   &    |- G = ( x e. A , y e. B |-> ( H ` C ) )   =>    |- ( H Fn D -> G = ( H o. F ) )
Theorem	oprab2co 6294*	Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by David Abernethy, 23-Apr-2013.)
|- ( ( x e. A /\ y e. B ) -> C e. R )   &    |- ( ( x e. A /\ y e. B ) -> D e. S )   &    |- F = ( x e. A , y e. B |-> <. C , D >. )   &    |- G = ( x e. A , y e. B |-> ( C M D ) )   =>    |- ( M Fn ( R X. S ) -> G = ( M o. F ) )
Theorem	df1st2 6295*	An alternate possible definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- { <. <. x , y >. , z >. | z = x } = ( 1st |` ( _V X. _V ) )
Theorem	df2nd2 6296*	An alternate possible definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- { <. <. x , y >. , z >. | z = y } = ( 2nd |` ( _V X. _V ) )
Theorem	1stconst 6297	The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008.)
|- ( B e. V -> ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -1-1-onto-> A )
Theorem	2ndconst 6298	The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008.)
|- ( A e. V -> ( 2nd |` ( { A } X. B ) ) : ( { A } X. B ) -1-1-onto-> B )
Theorem	dfmpo 6299*	Alternate definition for the maps-to notation df-mpo 5939 (although it requires that C be a set). (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- C e. _V   =>    |- ( x e. A , y e. B |-> C ) = U_ x e. A U_ y e. B { <. <. x , y >. , C >. }
Theorem	cnvf1olem 6300	Lemma for cnvf1o 6301. (Contributed by Mario Carneiro, 27-Apr-2014.)
|- ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> ( C e. `' A /\ B = U. `' { C } ) )