P. 72 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7101-7200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iprc 7101	The identity function is a proper class. This means, for example, that we cannot use it as a member of the class of continuous functions unless it is restricted to a set, as in idcn 21061. (Contributed by NM, 1-Jan-2007.)
|- -. _I e. _V
Theorem	resiexg 7102	The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 6479). (Contributed by NM, 13-Jan-2007.)
|- ( A e. V -> ( _I |` A ) e. _V )
Theorem	imaexg 7103	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.)
|- ( A e. V -> ( A " B ) e. _V )
Theorem	imaex 7104	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.)
|- A e. _V   =>    |- ( A " B ) e. _V
Theorem	exse2 7105	Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- ( R e. V -> R Se A )
Theorem	xpexr 7106	If a Cartesian product is a set, one of its components must be a set. (Contributed by NM, 27-Aug-2006.)
|- ( ( A X. B ) e. C -> ( A e. _V \/ B e. _V ) )
Theorem	xpexr2 7107	If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006.)
|- ( ( ( A X. B ) e. C /\ ( A X. B ) =/= (/) ) -> ( A e. _V /\ B e. _V ) )
Theorem	xpexcnv 7108	A condition where the converse of xpex 6962 holds as well. Corollary 6.9(2) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.)
|- ( ( B =/= (/) /\ ( A X. B ) e. _V ) -> A e. _V )
Theorem	soex 7109	If the relation in a strict order is a set, then the base field is also a set. (Contributed by Mario Carneiro, 27-Apr-2015.)
|- ( ( R Or A /\ R e. V ) -> A e. _V )
Theorem	elxp4 7110	Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 7111, elxp6 7200, and elxp7 7201. (Contributed by NM, 17-Feb-2004.)
|- ( A e. ( B X. C ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { A } e. B /\ U. ran { A } e. C ) ) )
Theorem	elxp5 7111	Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7110 when the double intersection does not create class existence problems (caused by int0 4490). (Contributed by NM, 1-Aug-2004.)
|- ( A e. ( B X. C ) <-> ( A = <. |^| |^| A , U. ran { A } >. /\ ( |^| |^| A e. B /\ U. ran { A } e. C ) ) )
Theorem	cnvexg 7112	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.)
|- ( A e. V -> `' A e. _V )
Theorem	cnvex 7113	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 19-Dec-2003.)
|- A e. _V   =>    |- `' A e. _V
Theorem	relcnvexb 7114	A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.)
|- ( Rel R -> ( R e. _V <-> `' R e. _V ) )
Theorem	f1oexrnex 7115	If the range of a 1-1 onto function is a set, the function itself is a set. (Contributed by AV, 2-Jun-2019.)
|- ( ( F : A -1-1-onto-> B /\ B e. V ) -> F e. _V )
Theorem	f1oexbi 7116*	There is a one-to-one onto function from a set to a second set iff there is a one-to-one onto function from the second set to the first set. (Contributed by Alexander van der Vekens, 30-Sep-2018.)
|- ( E. f f : A -1-1-onto-> B <-> E. g g : B -1-1-onto-> A )
Theorem	coexg 7117	The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)
|- ( ( A e. V /\ B e. W ) -> ( A o. B ) e. _V )
Theorem	coex 7118	The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- ( A o. B ) e. _V
Theorem	funcnvuni 7119*	The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 5958 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.)
|- ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> Fun `' U. A )
Theorem	fun11uni 7120*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by NM, 11-Aug-2004.)
|- ( A. f e. A ( ( Fun f /\ Fun `' f ) /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> ( Fun U. A /\ Fun `' U. A ) )
Theorem	fex2 7121	A function with bounded domain and range is a set. This version of fex 6490 is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( ( F : A --> B /\ A e. V /\ B e. W ) -> F e. _V )
Theorem	fabexg 7122*	Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.)
|- F = { x | ( x : A --> B /\ ph ) }   =>    |- ( ( A e. C /\ B e. D ) -> F e. _V )
Theorem	fabex 7123*	Existence of a set of functions. (Contributed by NM, 3-Dec-2007.)
|- A e. _V   &    |- B e. _V   &    |- F = { x | ( x : A --> B /\ ph ) }   =>    |- F e. _V
Theorem	dmfex 7124	If a mapping is a set, its domain is a set. (Contributed by NM, 27-Aug-2006.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|- ( ( F e. C /\ F : A --> B ) -> A e. _V )
Theorem	f1oabexg 7125*	The class of all 1-1-onto functions mapping one set to another is a set. (Contributed by Paul Chapman, 25-Feb-2008.)
|- F = { f | ( f : A -1-1-onto-> B /\ ph ) }   =>    |- ( ( A e. C /\ B e. D ) -> F e. _V )
Theorem	fun11iun 7126*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( x = y -> B = C )   &    |- B e. _V   =>    |- ( A. x e. A ( B : D -1-1-> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) -> U_ x e. A B : U_ x e. A D -1-1-> S )
Theorem	ffoss 7127*	Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by NM, 10-May-1998.)
|- F e. _V   =>    |- ( F : A --> B <-> E. x ( F : A -onto-> x /\ x C_ B ) )
Theorem	f11o 7128*	Relationship between one-to-one and one-to-one onto function. (Contributed by NM, 4-Apr-1998.)
|- F e. _V   =>    |- ( F : A -1-1-> B <-> E. x ( F : A -1-1-onto-> x /\ x C_ B ) )
Theorem	resfunexgALT 7129	Alternate proof of resfunexg 6479, shorter but requiring ax-pow 4843 and ax-un 6949. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( Fun A /\ B e. C ) -> ( A |` B ) e. _V )
Theorem	cofunexg 7130	Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.)
|- ( ( Fun A /\ B e. C ) -> ( A o. B ) e. _V )
Theorem	cofunex2g 7131	Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.)
|- ( ( A e. V /\ Fun `' B ) -> ( A o. B ) e. _V )
Theorem	fnexALT 7132	Alternate proof of fnex 6481, derived using the Axiom of Replacement in the form of funimaexg 5975. This version uses ax-pow 4843 and ax-un 6949, whereas fnex 6481 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( F Fn A /\ A e. B ) -> F e. _V )
Theorem	funrnex 7133	If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of funex 6482. (Contributed by NM, 11-Nov-1995.)
|- ( dom F e. B -> ( Fun F -> ran F e. _V ) )
Theorem	zfrep6 7134*	A version of the Axiom of Replacement. Normally ph would have free variables x and y. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4781 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep 4771. (Contributed by NM, 10-Oct-2003.)
|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )
Theorem	fornex 7135	If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.)
|- ( A e. C -> ( F : A -onto-> B -> B e. _V ) )
Theorem	f1dmex 7136	If the codomain of a one-to-one function exists, so does its domain. This theorem is equivalent to the Axiom of Replacement ax-rep 4771. (Contributed by NM, 4-Sep-2004.)
|- ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V )
Theorem	f1ovv 7137	The range of a 1-1 onto function is a set iff its domain is a set. (Contributed by AV, 21-Mar-2019.)
|- ( F : A -1-1-onto-> B -> ( A e. _V <-> B e. _V ) )
Theorem	fvclex 7138*	Existence of the class of values of a set. (Contributed by NM, 9-Nov-1995.)
|- F e. _V   =>    |- { y | E. x y = ( F ` x ) } e. _V
Theorem	fvresex 7139*	Existence of the class of values of a restricted class. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- A e. _V   =>    |- { y | E. x y = ( ( F |` A ) ` x ) } e. _V
Theorem	abrexexg 7140*	Existence of a class abstraction of existentially restricted sets. The class B can be thought of as an expression in x (which is typically a free variable in the class expression substituted for B) and the class abstraction appearing in the statement as the class of values B as x varies through A. If the "domain" A is a set, then the abstraction is also a set. Therefore, this statement is a kind of Replacement. This can be seen by tracing back through the path mptexg 6484, funex 6482, fnex 6481, resfunexg 6479, and funimaexg 5975. See also abrexex2g 7144. There are partial converses under additional conditions, see for instance abnexg 6964. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|- ( A e. V -> { y | E. x e. A y = B } e. _V )
Theorem	abrexex 7141*	Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7140. See also abrexex2 7148. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|- A e. _V   =>    |- { y | E. x e. A y = B } e. _V
Theorem	abrexexOLD 7142*	Obsolete proof of abrexex 7141 as of 8-Dec-2021. (Contributed by NM, 16-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A e. _V   =>    |- { y | E. x e. A y = B } e. _V
Theorem	iunexg 7143*	The existence of an indexed union. x is normally a free-variable parameter in B. (Contributed by NM, 23-Mar-2006.)
|- ( ( A e. V /\ A. x e. A B e. W ) -> U_ x e. A B e. _V )
Theorem	abrexex2g 7144*	Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( A e. V /\ A. x e. A { y | ph } e. W ) -> { y | E. x e. A ph } e. _V )
Theorem	opabex3d 7145*	Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.)
|- ( ph -> A e. _V )   &    |- ( ( ph /\ x e. A ) -> { y | ps } e. _V )   =>    |- ( ph -> { <. x , y >. | ( x e. A /\ ps ) } e. _V )
Theorem	opabex3 7146*	Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- A e. _V   &    |- ( x e. A -> { y | ph } e. _V )   =>    |- { <. x , y >. | ( x e. A /\ ph ) } e. _V
Theorem	iunex 7147*	The existence of an indexed union. x is normally a free-variable parameter in the class expression substituted for B, which can be read informally as B ( x ). (Contributed by NM, 13-Oct-2003.)
|- A e. _V   &    |- B e. _V   =>    |- U_ x e. A B e. _V
Theorem	abrexex2 7148*	Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x and y. See also abrexex 7141. (Contributed by NM, 12-Sep-2004.)
|- A e. _V   &    |- { y | ph } e. _V   =>    |- { y | E. x e. A ph } e. _V
Theorem	abexssex 7149*	Existence of a class abstraction with an existentially quantified expression. Both x and y can be free in ph. (Contributed by NM, 29-Jul-2006.)
|- A e. _V   &    |- { y | ph } e. _V   =>    |- { y | E. x ( x C_ A /\ ph ) } e. _V
Theorem	abrexex2OLD 7150*	Obsolete proof of abrexex2 7148 as of 8-Dec-2021. (Contributed by NM, 12-Sep-2004.) (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   &    |- { y | ph } e. _V   =>    |- { y | E. x e. A ph } e. _V
Theorem	abexex 7151*	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	f1oweALT 7152*	Alternate proof of f1owe 6603, more direct since not using the isomorphism predicate, but requiring ax-un 6949. (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	wemoiso 7153*	Thus, there is at most one isomorphism between any two well-ordered sets. TODO: Shorten finnisoeu 8936. (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 7154*	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	oprabexd 7155*	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 7156*	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 7157*	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 7158*	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 7159*	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 7141. (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 7160*	Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x, y, and z. Compare abrexex2 7148. (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 7161	Alternate proof of xpexg 6960 requiring Replacement (ax-rep 4771) but not Power Set (ax-pow 4843). (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 7162*	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 7163	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 7164*	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 7165, allowing it to be used as a function or structure argument. By ofmresval 6910, 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 7165	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 )
2.4.7  First and second members of an ordered pair
Syntax	c1st 7166	Extend the definition of a class to include the first member an ordered pair function.
class 1st
Syntax	c2nd 7167	Extend the definition of a class to include the second member an ordered pair function.
class 2nd
Definition	df-1st 7168	Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 7176 proves that it does this. For example, ( 1st ` <. 3 , 4 >. ) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 5617 and op1stb 4940). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 1st = ( x e. _V |-> U. dom { x } )
Definition	df-2nd 7169	Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 7177 proves that it does this. For example, ( 2nd ` <. 3 , 4 >. ) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 5620 and op2ndb 5619). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 2nd = ( x e. _V |-> U. ran { x } )
Theorem	1stval 7170	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.)
|- ( 1st ` A ) = U. dom { A }
Theorem	2ndval 7171	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.)
|- ( 2nd ` A ) = U. ran { A }
Theorem	1stnpr 7172	Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
|- ( -. A e. ( _V X. _V ) -> ( 1st ` A ) = (/) )
Theorem	2ndnpr 7173	Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
|- ( -. A e. ( _V X. _V ) -> ( 2nd ` A ) = (/) )
Theorem	1st0 7174	The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 1st ` (/) ) = (/)
Theorem	2nd0 7175	The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 2nd ` (/) ) = (/)
Theorem	op1st 7176	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 7177	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 7178	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 7179	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 7180	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 7181	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 7182	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 7182, ot2ndg 7183, ot3rdg 7184.) (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 7183	Extract the second member of an ordered triple. (See ot1stg 7182 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	ot3rdg 7184	Extract the third member of an ordered triple. (See ot1stg 7182 comment.) (Contributed by NM, 3-Apr-2015.)
|- ( C e. V -> ( 2nd ` <. A , B , C >. ) = C )
Theorem	1stval2 7185	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 7186	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	oteqimp 7187	The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
|- ( T = <. A , B , C >. -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( 1st ` ( 1st ` T ) ) = A /\ ( 2nd ` ( 1st ` T ) ) = B /\ ( 2nd ` T ) = C ) ) )
Theorem	fo1st 7188	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 7189	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 7190	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 7191	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	fo1stres 7192	Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 14-Dec-2008.)
|- ( B =/= (/) -> ( 1st |` ( A X. B ) ) : ( A X. B ) -onto-> A )
Theorem	fo2ndres 7193	Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 14-Dec-2008.)
|- ( A =/= (/) -> ( 2nd |` ( A X. B ) ) : ( A X. B ) -onto-> B )
Theorem	1st2val 7194*	Value of an alternate definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A )
Theorem	2nd2val 7195*	Value of an alternate definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( { <. <. x , y >. , z >. | z = y } ` A ) = ( 2nd ` A )
Theorem	1stcof 7196	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 7197	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 7198	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 7199	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	elxp6 7200	Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7110. (Contributed by NM, 9-Oct-2004.)
|- ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )