P. 47 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4601-4700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xpeq12i 4601	Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
|- A = B   &    |- C = D   =>    |- ( A X. C ) = ( B X. D )
Theorem	xpeq1d 4602	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A X. C ) = ( B X. C ) )
Theorem	xpeq2d 4603	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C X. A ) = ( C X. B ) )
Theorem	xpeq12d 4604	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 4605	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 4606	Bound-variable hypothesis builder for cross 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 4607	The empty set is not a member of a cross product. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- -. (/) e. ( A X. B )
Theorem	0nelelxp 4608	A member of a cross product (ordered pair) doesn't contain the empty set. (Contributed by NM, 15-Dec-2008.)
|- ( C e. ( A X. B ) -> -. (/) e. C )
Theorem	opelxp 4609	Ordered pair membership in a cross 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 4610	Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
|- ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )
Theorem	opelxpi 4611	Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)
|- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )
Theorem	opelxpd 4612	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 4613	The first member of an ordered pair of classes in a cross product belongs to first cross 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 4614	The second member of an ordered pair of classes in a cross product belongs to second cross product argument. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( <. A , B >. e. ( C X. D ) -> B e. D )
Theorem	otelxp1 4615	The first member of an ordered triple of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.)
|- ( <. <. A , B >. , C >. e. ( ( R X. S ) X. T ) -> A e. R )
Theorem	rabxp 4616*	Membership in a class builder restricted to a cross 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 4617	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	brrelex1 4618	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	brrelex 4619	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 4620	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	brrelex12i 4621	Two classes that are related by a binary relation are sets. (An artifact of our ordered pair definition.) (Contributed by BJ, 3-Oct-2022.)
|- Rel R   =>    |- ( A R B -> ( A e. _V /\ B e. _V ) )
Theorem	brrelex1i 4622	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 4623	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	nprrel 4624	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 4625	A binary relation does not contain the empty set. (Contributed by AV, 15-Nov-2021.)
|- ( Rel R -> (/) e/ R )
Theorem	fconstmpt 4626*	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 4627*	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 4628	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 4629	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 4630	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 4631	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	brab2a 4632*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 9-Nov-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	elxp3 4633*	Membership in a cross 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 4634	Membership in a union of cross 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 4635	Distributive law for cross 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 4636	Distributive law for cross 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 4637*	Distributive law for cross 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 4638*	Distributive law for cross 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 4639*	Membership in a union of cross 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 4640	The cross 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 4641*	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 4642*	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 4643	An ordered pair contains its union. (Contributed by NM, 16-Sep-2006.)
|- ( A e. ( _V X. _V ) -> U. A e. A )
Theorem	mosubopt 4644*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
|- ( A. y A. z E* x ph -> E* x E. y E. z ( A = <. y , z >. /\ ph ) )
Theorem	mosubop 4645*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
|- E* x ph   =>    |- E* x E. y E. z ( A = <. y , z >. /\ ph )
Theorem	brinxp2 4646	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 4647	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 4648	Intersection of partial order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
|- ( R Po A <-> ( R i^i ( A X. A ) ) Po A )
Theorem	soinxp 4649	Intersection of linear order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
|- ( R Or A <-> ( R i^i ( A X. A ) ) Or A )
Theorem	seinxp 4650	Intersection of set-like relation with cross product of its field. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- ( R Se A <-> ( R i^i ( A X. A ) ) Se A )
Theorem	posng 4651	Partial ordering of a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
|- ( ( Rel R /\ A e. _V ) -> ( R Po { A } <-> -. A R A ) )
Theorem	sosng 4652	Strict linear ordering on a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
|- ( ( Rel R /\ A e. _V ) -> ( R Or { A } <-> -. A R A ) )
Theorem	opabssxp 4653*	An abstraction relation is a subset of a related cross product. (Contributed by NM, 16-Jul-1995.)
|- { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )
Theorem	brab2ga 4654*	The law of concretion for a binary relation. See brab2a 4632 for alternate proof. TODO: should one of them be deleted? (Contributed by Mario Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
|- ( ( 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 4655*	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 4656*	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 4657*	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 4658*	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 4659	The cross 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	csbxpg 4660	Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. D -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) )
Theorem	releq 4661	Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
|- ( A = B -> ( Rel A <-> Rel B ) )
Theorem	releqi 4662	Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
|- A = B   =>    |- ( Rel A <-> Rel B )
Theorem	releqd 4663	Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> ( Rel A <-> Rel B ) )
Theorem	nfrel 4664	Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   =>    |- F/ x Rel A
Theorem	sbcrel 4665	Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
|- ( A e. V -> ( [. A / x ]. Rel R <-> Rel [_ A / x ]_ R ) )
Theorem	relss 4666	Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
|- ( A C_ B -> ( Rel B -> Rel A ) )
Theorem	ssrel 4667*	A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
Theorem	eqrel 4668*	Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.)
|- ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
Theorem	ssrel2 4669*	A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4667 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.)
|- ( R C_ ( A X. B ) -> ( R C_ S <-> A. x e. A A. y e. B ( <. x , y >. e. R -> <. x , y >. e. S ) ) )
Theorem	relssi 4670*	Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.)
|- Rel A   &    |- ( <. x , y >. e. A -> <. x , y >. e. B )   =>    |- A C_ B
Theorem	relssdv 4671*	Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.)
|- ( ph -> Rel A )   &    |- ( ph -> ( <. x , y >. e. A -> <. x , y >. e. B ) )   =>    |- ( ph -> A C_ B )
Theorem	eqrelriv 4672*	Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.)
|- ( <. x , y >. e. A <-> <. x , y >. e. B )   =>    |- ( ( Rel A /\ Rel B ) -> A = B )
Theorem	eqrelriiv 4673*	Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)
|- Rel A   &    |- Rel B   &    |- ( <. x , y >. e. A <-> <. x , y >. e. B )   =>    |- A = B
Theorem	eqbrriv 4674*	Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.)
|- Rel A   &    |- Rel B   &    |- ( x A y <-> x B y )   =>    |- A = B
Theorem	eqrelrdv 4675*	Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.)
|- Rel A   &    |- Rel B   &    |- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )   =>    |- ( ph -> A = B )
Theorem	eqbrrdv 4676*	Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> Rel A )   &    |- ( ph -> Rel B )   &    |- ( ph -> ( x A y <-> x B y ) )   =>    |- ( ph -> A = B )
Theorem	eqbrrdiv 4677*	Deduction from extensionality principle for relations. (Contributed by Rodolfo Medina, 10-Oct-2010.)
|- Rel A   &    |- Rel B   &    |- ( ph -> ( x A y <-> x B y ) )   =>    |- ( ph -> A = B )
Theorem	eqrelrdv2 4678*	A version of eqrelrdv 4675. (Contributed by Rodolfo Medina, 10-Oct-2010.)
|- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )   =>    |- ( ( ( Rel A /\ Rel B ) /\ ph ) -> A = B )
Theorem	ssrelrel 4679*	A subclass relationship determined by ordered triples. Use relrelss 5105 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A C_ ( ( _V X. _V ) X. _V ) -> ( A C_ B <-> A. x A. y A. z ( <. <. x , y >. , z >. e. A -> <. <. x , y >. , z >. e. B ) ) )
Theorem	eqrelrel 4680*	Extensionality principle for ordered triples, analogous to eqrel 4668. Use relrelss 5105 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.)
|- ( ( A u. B ) C_ ( ( _V X. _V ) X. _V ) -> ( A = B <-> A. x A. y A. z ( <. <. x , y >. , z >. e. A <-> <. <. x , y >. , z >. e. B ) ) )
Theorem	elrel 4681*	A member of a relation is an ordered pair. (Contributed by NM, 17-Sep-2006.)
|- ( ( Rel R /\ A e. R ) -> E. x E. y A = <. x , y >. )
Theorem	relsng 4682	A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.) (Revised by BJ, 12-Feb-2022.)
|- ( A e. V -> ( Rel { A } <-> A e. ( _V X. _V ) ) )
Theorem	relsnopg 4683	A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by BJ, 12-Feb-2022.)
|- ( ( A e. V /\ B e. W ) -> Rel { <. A , B >. } )
Theorem	relsn 4684	A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.)
|- A e. _V   =>    |- ( Rel { A } <-> A e. ( _V X. _V ) )
Theorem	relsnop 4685	A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- Rel { <. A , B >. }
Theorem	xpss12 4686	Subset theorem for cross product. Generalization of Theorem 101 of [Suppes] p. 52. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )
Theorem	xpss 4687	A cross product is included in the ordered pair universe. Exercise 3 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
|- ( A X. B ) C_ ( _V X. _V )
Theorem	relxp 4688	A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.)
|- Rel ( A X. B )
Theorem	xpss1 4689	Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( A C_ B -> ( A X. C ) C_ ( B X. C ) )
Theorem	xpss2 4690	Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ( A C_ B -> ( C X. A ) C_ ( C X. B ) )
Theorem	xpsspw 4691	A cross product is included in the power of the power of the union of its arguments. (Contributed by NM, 13-Sep-2006.)
|- ( A X. B ) C_ ~P ~P ( A u. B )
Theorem	unixpss 4692	The double class union of a cross product is included in the union of its arguments. (Contributed by NM, 16-Sep-2006.)
|- U. U. ( A X. B ) C_ ( A u. B )
Theorem	xpexg 4693	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
Theorem	xpex 4694	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
|- A e. _V   &    |- B e. _V   =>    |- ( A X. B ) e. _V
Theorem	sqxpexg 4695	The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.)
|- ( A e. V -> ( A X. A ) e. _V )
Theorem	relun 4696	The union of two relations is a relation. Compare Exercise 5 of [TakeutiZaring] p. 25. (Contributed by NM, 12-Aug-1994.)
|- ( Rel ( A u. B ) <-> ( Rel A /\ Rel B ) )
Theorem	relin1 4697	The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994.)
|- ( Rel A -> Rel ( A i^i B ) )
Theorem	relin2 4698	The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006.)
|- ( Rel B -> Rel ( A i^i B ) )
Theorem	reldif 4699	A difference cutting down a relation is a relation. (Contributed by NM, 31-Mar-1998.)
|- ( Rel A -> Rel ( A \ B ) )
Theorem	reliun 4700	An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.)
|- ( Rel U_ x e. A B <-> A. x e. A Rel B )