P. 62 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6101-6200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ofco 6101	The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> H : D --> C )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> D e. X )   &    |- ( A i^i B ) = C   =>    |- ( ph -> ( ( F oF R G ) o. H ) = ( ( F o. H ) oF R ( G o. H ) ) )
Theorem	offveqb 6102*	Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   &    |- ( ph -> H Fn A )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )   &    |- ( ( ph /\ x e. A ) -> ( G ` x ) = C )   =>    |- ( ph -> ( H = ( F oF R G ) <-> A. x e. A ( H ` x ) = ( B R C ) ) )
Theorem	ofc12 6103	Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   =>    |- ( ph -> ( ( A X. { B } ) oF R ( A X. { C } ) ) = ( A X. { ( B R C ) } ) )
Theorem	caofref 6104*	Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ( ph /\ x e. S ) -> x R x )   =>    |- ( ph -> F oR R F )
Theorem	caofinvl 6105*	Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ph -> N : S --> S )   &    |- ( ph -> G = ( v e. A |-> ( N ` ( F ` v ) ) ) )   &    |- ( ( ph /\ x e. S ) -> ( ( N ` x ) R x ) = B )   =>    |- ( ph -> ( G oF R F ) = ( A X. { B } ) )
Theorem	caofcom 6106*	Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y ) = ( y R x ) )   =>    |- ( ph -> ( F oF R G ) = ( G oF R F ) )
Theorem	caofrss 6107*	Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y -> x T y ) )   =>    |- ( ph -> ( F oR R G -> F oR T G ) )
Theorem	caoftrn 6108*	Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ph -> H : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x R y /\ y T z ) -> x U z ) )   =>    |- ( ph -> ( ( F oR R G /\ G oR T H ) -> F oR U H ) )
2.6.14  Functions (continued)
Theorem	resfunexgALT 6109	The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. This version has a shorter proof than resfunexg 5738 but requires ax-pow 4175 and ax-un 4434. (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 6110	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 6111	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 6112	If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of funimaexg 5301. This version of fnex 5739 uses ax-pow 4175 and ax-un 4434, whereas fnex 5739 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	funexw 6113	Weak version of funex 5740 that holds without ax-coll 4119. If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023.)
|- ( ( Fun F /\ dom F e. B /\ ran F e. C ) -> F e. _V )
Theorem	mptexw 6114*	Weak version of mptex 5743 that holds without ax-coll 4119. If the domain and codomain of a function given by maps-to notation are sets, the function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
|- A e. _V   &    |- C e. _V   &    |- A. x e. A B e. C   =>    |- ( x e. A |-> B ) e. _V
Theorem	funrnex 6115	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 5740. (Contributed by NM, 11-Nov-1995.)
|- ( dom F e. B -> ( Fun F -> ran F e. _V ) )
Theorem	focdmex 6116	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 6117	If the codomain of a one-to-one function exists, so does its domain. This can be thought of as a form of the Axiom of Replacement. (Contributed by NM, 4-Sep-2004.)
|- ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V )
Theorem	abrexex 6118*	Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in the class expression substituted for B, which can be thought of as B ( x ). This simple-looking theorem is actually quite powerful and appears to involve the Axiom of Replacement in an intrinsic way, as can be seen by tracing back through the path mptexg 5742, funex 5740, fnex 5739, resfunexg 5738, and funimaexg 5301. See also abrexex2 6125. (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	abrexexg 6119*	Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in B. The antecedent assures us that A is a set. (Contributed by NM, 3-Nov-2003.)
|- ( A e. V -> { y | E. x e. A y = B } e. _V )
Theorem	iunexg 6120*	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 6121*	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 6122*	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 6123*	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 6124*	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 6125*	Existence of an existentially restricted class abstraction. ph is normally has free-variable parameters x and y. See also abrexex 6118. (Contributed by NM, 12-Sep-2004.)
|- A e. _V   &    |- { y | ph } e. _V   =>    |- { y | E. x e. A ph } e. _V
Theorem	abexssex 6126*	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	abexex 6127*	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 6128*	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 6129*	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 6130*	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 6131*	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 6132*	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 6118. (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 6133*	Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x, y, and z. Compare abrexex2 6125. (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 6134	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. This version is proven using Replacement; see xpexg 4741 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 6135*	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 6136	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 6137*	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 6138, allowing it to be used as a function or structure argument. By ofmresval 6094, 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 6138	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.6.15  First and second members of an ordered pair
Syntax	c1st 6139	Extend the definition of a class to include the first member an ordered pair function.
class 1st
Syntax	c2nd 6140	Extend the definition of a class to include the second member an ordered pair function.
class 2nd
Definition	df-1st 6141	Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 6147 proves that it does this. For example, ( 1st ` <. 3 , 4 >.) = 3 . Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 5111 and op1stb 4479). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 1st = ( x e. _V |-> U. dom { x } )
Definition	df-2nd 6142	Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 6148 proves that it does this. For example, ( 2nd ` <. 3 , 4 >.) = 4 . Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 5114 and op2ndb 5113). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 2nd = ( x e. _V |-> U. ran { x } )
Theorem	1stvalg 6143	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 6144	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 6145	The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 1st ` (/) ) = (/)
Theorem	2nd0 6146	The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 2nd ` (/) ) = (/)
Theorem	op1st 6147	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 6148	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 6149	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 6150	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 6151	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 6152	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 6153	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 6153, ot2ndg 6154, ot3rdgg 6155.) (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 6154	Extract the second member of an ordered triple. (See ot1stg 6153 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 6155	Extract the third member of an ordered triple. (See ot1stg 6153 comment.) (Contributed by NM, 3-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( 2nd ` <. A , B , C >. ) = C )
Theorem	1stval2 6156	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 6157	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 6158	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 6159	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 6160	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 6161	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 6162*	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 6163*	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 6164	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 6165	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 6166	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 6167	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 6168	Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.)
|- ( A e. V -> ( 1st ` A ) e. _V )
Theorem	2ndexg 6169	Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.)
|- ( A e. V -> ( 2nd ` A ) e. _V )
Theorem	elxp6 6170	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp4 5117. (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 6171	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp4 5117. (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 6172*	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 6173	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 6174*	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 6175	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 6176	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 6177	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 6178	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 6179	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 6180*	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 6181	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 6182	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 6183	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 6184	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 6185	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 6186*	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 6187*	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 6188	Equality theorem for substitution of a class for an ordered pair (analog of sbceq1a 2973 that avoids the existential quantifiers of copsexg 4245). (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 6189	Equality theorem for substitution of a class A for an ordered pair <. x , y >. in B (analog of csbeq1a 3067). (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 6190*	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 6191*	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 6192*	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 6193*	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 6194*	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 6195*	Define the cross product of three classes. Compare df-xp 4633. (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 6196*	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 6197*	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 6198*	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 6199*	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 6200*	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 )