P. 52 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5101-5200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wess 5101	Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31. (Contributed by NM, 19-Apr-1994.)
|- ( A C_ B -> ( R We B -> R We A ) )
Theorem	weeq1 5102	Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R We A <-> S We A ) )
Theorem	weeq2 5103	Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R We A <-> R We B ) )
Theorem	wefr 5104	A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
|- ( R We A -> R Fr A )
Theorem	weso 5105	A well-ordering is a strict ordering. (Contributed by NM, 16-Mar-1997.)
|- ( R We A -> R Or A )
Theorem	wecmpep 5106	The elements of an epsilon well-ordering are comparable. (Contributed by NM, 17-May-1994.)
|- ( ( _E We A /\ ( x e. A /\ y e. A ) ) -> ( x e. y \/ x = y \/ y e. x ) )
Theorem	wetrep 5107	An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.)
|- ( ( _E We A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x e. y /\ y e. z ) -> x e. z ) )
Theorem	wefrc 5108*	A nonempty (possibly proper) subclass of a class well-ordered by _E has a minimal element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by NM, 17-Feb-2004.)
|- ( ( _E We A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )
Theorem	we0 5109	Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.)
|- R We (/)
Theorem	wereu 5110*	A subset of a well-ordered set has a unique minimal element. (Contributed by NM, 18-Mar-1997.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( R We A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E! x e. B A. y e. B -. y R x )
Theorem	wereu2 5111*	All nonempty (possibly proper) subclasses of A, which has a well-founded relation R, have R-minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E! x e. B A. y e. B -. y R x )
2.3.10  Relations
Syntax	cxp 5112	Extend the definition of a class to include the Cartesian product.
class ( A X. B )
Syntax	ccnv 5113	Extend the definition of a class to include the converse of a class.
class `' A
Syntax	cdm 5114	Extend the definition of a class to include the domain of a class.
class dom A
Syntax	crn 5115	Extend the definition of a class to include the range of a class.
class ran A
Syntax	cres 5116	Extend the definition of a class to include the restriction of a class. (Read: The restriction of A to B.)
class ( A |` B )
Syntax	cima 5117	Extend the definition of a class to include the image of a class. (Read: The image of B under A.)
class ( A " B )
Syntax	ccom 5118	Extend the definition of a class to include the composition of two classes. (Read: The composition of A and B.)
class ( A o. B )
Syntax	wrel 5119	Extend the definition of a wff to include the relation predicate. (Read: A is a relation.)
wff Rel A
Definition	df-xp 5120*	Define the Cartesian product of two classes. This is also sometimes called the "cross product" but that term also has other meanings; we intentionally choose a less ambiguous term. Definition 9.11 of [Quine] p. 64. For example, ( { 1 , 5 } X. { 2 , 7 } ) = ( { <. 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } ) (ex-xp 27293). Another example is that the set of rational numbers are defined in df-q 11789 using the Cartesian product ( ZZ X. NN ); the left- and right-hand sides of the Cartesian product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994.)
|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
Definition	df-rel 5121	Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5583 and dfrel3 5592. (Contributed by NM, 1-Aug-1994.)
|- ( Rel A <-> A C_ ( _V X. _V ) )
Definition	df-cnv 5122*	Define the converse of a class. Definition 9.12 of [Quine] p. 64. The converse of a binary relation swaps its arguments, i.e., if A e. _V and B e. _V then ( A `' R B <-> B R A ), as proven in brcnv 5305 (see df-br 4654 and df-rel 5121 for more on relations). For example, `' { <. 2 , 6 >. , <. 3 , 9 >. } = { <. 6 , 2 >. , <. 9 , 3 >. } (ex-cnv 27294). We use Quine's breve accent (smile) notation. Like Quine, we use it as a prefix, which eliminates the need for parentheses. Many authors use the postfix superscript "to the minus one." "Converse" is Quine's terminology; some authors call it "inverse," especially when the argument is a function. (Contributed by NM, 4-Jul-1994.)
|- `' A = { <. x , y >. | y A x }
Definition	df-co 5123*	Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ( ( exp o. cos ) ` 0 ) = _e (ex-co 27295) because ( cos ` 0 ) = 1 (see cos0 14880) and ( exp ` 1 ) = _e (see df-e 14799). Note that Definition 7 of [Suppes] p. 63 reverses A and B, uses /. instead of o., and calls the operation "relative product." (Contributed by NM, 4-Jul-1994.)
|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
Definition	df-dm 5124*	Define the domain of a class. Definition 3 of [Suppes] p. 59. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> dom F = { 2 , 3 } (ex-dm 27296). Another example is the domain of the complex arctangent, ( A e. dom arctan <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) ) (for proof see atandm 24603). Contrast with range (defined in df-rn 5125). For alternate definitions see dfdm2 5667, dfdm3 5310, and dfdm4 5316. The notation " dom " is used by Enderton; other authors sometimes use script D. (Contributed by NM, 1-Aug-1994.)
|- dom A = { x | E. y x A y }
Definition	df-rn 5125	Define the range of a class. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ran F = { 6 , 9 } (ex-rn 27297). Contrast with domain (defined in df-dm 5124). For alternate definitions, see dfrn2 5311, dfrn3 5312, and dfrn4 5595. The notation " ran " is used by Enderton; other authors sometimes use script R or script W. (Contributed by NM, 1-Aug-1994.)
|- ran A = dom `' A
Definition	df-res 5126	Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression ( exp |` RR ) (used in reeff1 14850) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14798 defines the exponential function, which normally allows the exponent to be a complex number). Another example is that ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F |` B ) = { <. 2 , 6 >. } (ex-res 27298). (Contributed by NM, 2-Aug-1994.)
|- ( A |` B ) = ( A i^i ( B X. _V ) )
Definition	df-ima 5127	Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F " B ) = { 6 } (ex-ima 27299). Contrast with restriction (df-res 5126) and range (df-rn 5125). For an alternate definition, see dfima2 5468. (Contributed by NM, 2-Aug-1994.)
|- ( A " B ) = ran ( A |` B )
Theorem	xpeq1 5128	Equality theorem for Cartesian product. (Contributed by NM, 4-Jul-1994.)
|- ( A = B -> ( A X. C ) = ( B X. C ) )
Theorem	xpeq2 5129	Equality theorem for Cartesian product. (Contributed by NM, 5-Jul-1994.)
|- ( A = B -> ( C X. A ) = ( C X. B ) )
Theorem	elxpi 5130*	Membership in a Cartesian product. Uses fewer axioms than elxp 5131. (Contributed by NM, 4-Jul-1994.)
|- ( A e. ( B X. C ) -> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
Theorem	elxp 5131*	Membership in a Cartesian product. (Contributed by NM, 4-Jul-1994.)
|- ( A e. ( B X. C ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. B /\ y e. C ) ) )
Theorem	elxp2 5132*	Membership in a Cartesian product. (Contributed by NM, 23-Feb-2004.) (Proof shortened by JJ, 13-Aug-2021.)
|- ( A e. ( B X. C ) <-> E. x e. B E. y e. C A = <. x , y >. )
Theorem	elxp2OLD 5133*	Obsolete proof of elxp2 5132 as of 13-Aug-2021. (Contributed by NM, 23-Feb-2004.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. ( B X. C ) <-> E. x e. B E. y e. C A = <. x , y >. )
Theorem	xpeq12 5134	Equality theorem for Cartesian product. (Contributed by FL, 31-Aug-2009.)
|- ( ( A = B /\ C = D ) -> ( A X. C ) = ( B X. D ) )
Theorem	xpeq1i 5135	Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( A X. C ) = ( B X. C )
Theorem	xpeq2i 5136	Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( C X. A ) = ( C X. B )
Theorem	xpeq12i 5137	Equality inference for Cartesian product. (Contributed by FL, 31-Aug-2009.)
|- A = B   &    |- C = D   =>    |- ( A X. C ) = ( B X. D )
Theorem	xpeq1d 5138	Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A X. C ) = ( B X. C ) )
Theorem	xpeq2d 5139	Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C X. A ) = ( C X. B ) )
Theorem	xpeq12d 5140	Equality deduction for Cartesian product. (Contributed by NM, 8-Dec-2013.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A X. C ) = ( B X. D ) )
Theorem	sqxpeqd 5141	Equality deduction for a Cartesian square, see Wikipedia "Cartesian product", https://en.wikipedia.org/wiki/Cartesian_product#n-ary_Cartesian_power. (Contributed by AV, 13-Jan-2020.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A X. A ) = ( B X. B ) )
Theorem	nfxp 5142	Bound-variable hypothesis builder for Cartesian product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A X. B )
Theorem	0nelxp 5143	The empty set is not a member of a Cartesian product. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof shortened by JJ, 13-Aug-2021.)
|- -. (/) e. ( A X. B )
Theorem	0nelxpOLD 5144	Obsolete proof of 0nelxp 5143 as of 13-Aug-2021. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
|- -. (/) e. ( A X. B )
Theorem	0nelelxp 5145	A member of a Cartesian product (ordered pair) doesn't contain the empty set. (Contributed by NM, 15-Dec-2008.)
|- ( C e. ( A X. B ) -> -. (/) e. C )
Theorem	opelxp 5146	Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
Theorem	brxp 5147	Binary relation on a Cartesian product. (Contributed by NM, 22-Apr-2004.)
|- ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )
Theorem	opelxpi 5148	Ordered pair membership in a Cartesian product (implication). (Contributed by NM, 28-May-1995.)
|- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )
Theorem	opelxpd 5149	Ordered pair membership in a Cartesian product, deduction form. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. D )   =>    |- ( ph -> <. A , B >. e. ( C X. D ) )
Theorem	opelxp1 5150	The first member of an ordered pair of classes in a Cartesian product belongs to first Cartesian product argument. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( <. A , B >. e. ( C X. D ) -> A e. C )
Theorem	opelxp2 5151	The second member of an ordered pair of classes in a Cartesian product belongs to second Cartesian product argument. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( <. A , B >. e. ( C X. D ) -> B e. D )
Theorem	otelxp1 5152	The first member of an ordered triple of classes in a Cartesian product belongs to first Cartesian product argument. (Contributed by NM, 28-May-2008.)
|- ( <. <. A , B >. , C >. e. ( ( R X. S ) X. T ) -> A e. R )
Theorem	otel3xp 5153	An ordered triple is an element of a doubled Cartesian product. (Contributed by Alexander van der Vekens, 26-Feb-2018.)
|- ( ( T = <. A , B , C >. /\ ( A e. X /\ B e. Y /\ C e. Z ) ) -> T e. ( ( X X. Y ) X. Z ) )
Theorem	rabxp 5154*	Membership in a class builder restricted to a Cartesian product. (Contributed by NM, 20-Feb-2014.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- { x e. ( A X. B ) | ph } = { <. y , z >. | ( y e. A /\ z e. B /\ ps ) }
Theorem	brrelex12 5155	A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) )
Theorem	brrelex 5156	A true binary relation on a relation implies the first argument is a set. (This is a property of our ordered pair definition.) (Contributed by NM, 18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( Rel R /\ A R B ) -> A e. _V )
Theorem	brrelex2 5157	A true binary relation on a relation implies the second argument is a set. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( Rel R /\ A R B ) -> B e. _V )
Theorem	brrelexi 5158	The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.)
|- Rel R   =>    |- ( A R B -> A e. _V )
Theorem	brrelex2i 5159	The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
|- Rel R   =>    |- ( A R B -> B e. _V )
Theorem	nprrel12 5160	Proper classes are not related via any relation. (Contributed by AV, 29-Oct-2021.)
|- Rel R   =>    |- ( -. ( A e. _V /\ B e. _V ) -> -. A R B )
Theorem	nprrel 5161	No proper class is related to anything via any relation. (Contributed by Roy F. Longton, 30-Jul-2005.)
|- Rel R   &    |- -. A e. _V   =>    |- -. A R B
Theorem	0nelrel 5162	A binary relation does not contain the empty set. (Contributed by AV, 15-Nov-2021.)
|- ( Rel R -> (/) e/ R )
Theorem	fconstmpt 5163*	Representation of a constant function using the mapping operation. (Note that x cannot appear free in B.) (Contributed by NM, 12-Oct-1999.) (Revised by Mario Carneiro, 16-Nov-2013.)
|- ( A X. { B } ) = ( x e. A |-> B )
Theorem	vtoclr 5164*	Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- Rel R   &    |- ( ( x R y /\ y R z ) -> x R z )   =>    |- ( ( A R B /\ B R C ) -> A R C )
Theorem	opelvvg 5165	Ordered pair membership in the universal class of ordered pairs. (Contributed by Mario Carneiro, 3-May-2015.)
|- ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( _V X. _V ) )
Theorem	opelvv 5166	Ordered pair membership in the universal class of ordered pairs. (Contributed by NM, 22-Aug-2013.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- <. A , B >. e. ( _V X. _V )
Theorem	opthprc 5167	Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in [Jech] p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003.)
|- ( ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ) = ( ( C X. { (/) } ) u. ( D X. { { (/) } } ) ) <-> ( A = C /\ B = D ) )
Theorem	brel 5168	Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- R C_ ( C X. D )   =>    |- ( A R B -> ( A e. C /\ B e. D ) )
Theorem	elxp3 5169*	Membership in a Cartesian product. (Contributed by NM, 5-Mar-1995.)
|- ( A e. ( B X. C ) <-> E. x E. y ( <. x , y >. = A /\ <. x , y >. e. ( B X. C ) ) )
Theorem	opeliunxp 5170	Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
|- ( <. x , C >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ C e. B ) )
Theorem	xpundi 5171	Distributive law for Cartesian product over union. Theorem 103 of [Suppes] p. 52. (Contributed by NM, 12-Aug-2004.)
|- ( A X. ( B u. C ) ) = ( ( A X. B ) u. ( A X. C ) )
Theorem	xpundir 5172	Distributive law for Cartesian product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
|- ( ( A u. B ) X. C ) = ( ( A X. C ) u. ( B X. C ) )
Theorem	xpiundi 5173*	Distributive law for Cartesian product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
|- ( C X. U_ x e. A B ) = U_ x e. A ( C X. B )
Theorem	xpiundir 5174*	Distributive law for Cartesian product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
|- ( U_ x e. A B X. C ) = U_ x e. A ( B X. C )
Theorem	iunxpconst 5175*	Membership in a union of Cartesian products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- U_ x e. A ( { x } X. B ) = ( A X. B )
Theorem	xpun 5176	The Cartesian product of two unions. (Contributed by NM, 12-Aug-2004.)
|- ( ( A u. B ) X. ( C u. D ) ) = ( ( ( A X. C ) u. ( A X. D ) ) u. ( ( B X. C ) u. ( B X. D ) ) )
Theorem	elvv 5177*	Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.)
|- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )
Theorem	elvvv 5178*	Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008.)
|- ( A e. ( ( _V X. _V ) X. _V ) <-> E. x E. y E. z A = <. <. x , y >. , z >. )
Theorem	elvvuni 5179	An ordered pair contains its union. (Contributed by NM, 16-Sep-2006.)
|- ( A e. ( _V X. _V ) -> U. A e. A )
Theorem	brinxp2 5180	Intersection of binary relation with Cartesian product. (Contributed by NM, 3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A ( R i^i ( C X. D ) ) B <-> ( A e. C /\ B e. D /\ A R B ) )
Theorem	brinxp 5181	Intersection of binary relation with Cartesian product. (Contributed by NM, 9-Mar-1997.)
|- ( ( A e. C /\ B e. D ) -> ( A R B <-> A ( R i^i ( C X. D ) ) B ) )
Theorem	poinxp 5182	Intersection of partial order with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
|- ( R Po A <-> ( R i^i ( A X. A ) ) Po A )
Theorem	soinxp 5183	Intersection of total order with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
|- ( R Or A <-> ( R i^i ( A X. A ) ) Or A )
Theorem	frinxp 5184	Intersection of well-founded relation with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
|- ( R Fr A <-> ( R i^i ( A X. A ) ) Fr A )
Theorem	seinxp 5185	Intersection of set-like relation with Cartesian product of its field. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- ( R Se A <-> ( R i^i ( A X. A ) ) Se A )
Theorem	weinxp 5186	Intersection of well-ordering with Cartesian product of its field. (Contributed by NM, 9-Mar-1997.) (Revised by Mario Carneiro, 10-Jul-2014.)
|- ( R We A <-> ( R i^i ( A X. A ) ) We A )
Theorem	posn 5187	Partial ordering of a singleton. (Contributed by NM, 27-Apr-2009.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( Rel R -> ( R Po { A } <-> -. A R A ) )
Theorem	sosn 5188	Strict ordering on a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- ( Rel R -> ( R Or { A } <-> -. A R A ) )
Theorem	frsn 5189	Founded relation on a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( Rel R -> ( R Fr { A } <-> -. A R A ) )
Theorem	wesn 5190	Well-ordering of a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- ( Rel R -> ( R We { A } <-> -. A R A ) )
Theorem	elopaelxp 5191*	Membership in an ordered pair class builder implies membership in a Cartesian product. (Contributed by Alexander van der Vekens, 23-Jun-2018.)
|- ( A e. { <. x , y >. | ps } -> A e. ( _V X. _V ) )
Theorem	bropaex12 5192*	Two classes related by an ordered pair class builder are sets. (Contributed by AV, 21-Jan-2020.)
|- R = { <. x , y >. | ps }   =>    |- ( A R B -> ( A e. _V /\ B e. _V ) )
Theorem	opabssxp 5193*	An abstraction relation is a subset of a related Cartesian product. (Contributed by NM, 16-Jul-1995.)
|- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )
Theorem	brab2a 5194*	The law of concretion for a binary relation. Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) }   =>    |- ( A R B <-> ( ( A e. C /\ B e. D ) /\ ps ) )
Theorem	optocl 5195*	Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.)
|- D = ( B X. C )   &    |- ( <. x , y >. = A -> ( ph <-> ps ) )   &    |- ( ( x e. B /\ y e. C ) -> ph )   =>    |- ( A e. D -> ps )
Theorem	2optocl 5196*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- R = ( C X. D )   &    |- ( <. x , y >. = A -> ( ph <-> ps ) )   &    |- ( <. z , w >. = B -> ( ps <-> ch ) )   &    |- ( ( ( x e. C /\ y e. D ) /\ ( z e. C /\ w e. D ) ) -> ph )   =>    |- ( ( A e. R /\ B e. R ) -> ch )
Theorem	3optocl 5197*	Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- R = ( D X. F )   &    |- ( <. x , y >. = A -> ( ph <-> ps ) )   &    |- ( <. z , w >. = B -> ( ps <-> ch ) )   &    |- ( <. v , u >. = C -> ( ch <-> th ) )   &    |- ( ( ( x e. D /\ y e. F ) /\ ( z e. D /\ w e. F ) /\ ( v e. D /\ u e. F ) ) -> ph )   =>    |- ( ( A e. R /\ B e. R /\ C e. R ) -> th )
Theorem	opbrop 5198*	Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.)
|- ( ( ( z = A /\ w = B ) /\ ( v = C /\ u = D ) ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ph ) ) }   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. R <. C , D >. <-> ps ) )
Theorem	0xp 5199	The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.)
|- ( (/) X. A ) = (/)
Theorem	csbxp 5200	Distribute proper substitution through the Cartesian product of two classes. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 23-Aug-2018.)
|- [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C )