P. 51 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dmresi 5001	The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)
|- dom ( _I |` A ) = A
Theorem	restidsing 5002	Restriction of the identity to a singleton. (Contributed by FL, 2-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.) (Proof shortened by Peter Mazsa, 6-Oct-2022.)
|- ( _I |` { A } ) = ( { A } X. { A } )
Theorem	resid 5003	Any relation restricted to the universe is itself. (Contributed by NM, 16-Mar-2004.)
|- ( Rel A -> ( A |` _V ) = A )
Theorem	imaeq1 5004	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|- ( A = B -> ( A " C ) = ( B " C ) )
Theorem	imaeq2 5005	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|- ( A = B -> ( C " A ) = ( C " B ) )
Theorem	imaeq1i 5006	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( A " C ) = ( B " C )
Theorem	imaeq2i 5007	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( C " A ) = ( C " B )
Theorem	imaeq1d 5008	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A " C ) = ( B " C ) )
Theorem	imaeq2d 5009	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C " A ) = ( C " B ) )
Theorem	imaeq12d 5010	Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A " C ) = ( B " D ) )
Theorem	dfima2 5011*	Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 19-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A " B ) = { y | E. x e. B x A y }
Theorem	dfima3 5012*	Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A " B ) = { y | E. x ( x e. B /\ <. x , y >. e. A ) }
Theorem	elimag 5013*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 20-Jan-2007.)
|- ( A e. V -> ( A e. ( B " C ) <-> E. x e. C x B A ) )
Theorem	elima 5014*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.)
|- A e. _V   =>    |- ( A e. ( B " C ) <-> E. x e. C x B A )
Theorem	elima2 5015*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.)
|- A e. _V   =>    |- ( A e. ( B " C ) <-> E. x ( x e. C /\ x B A ) )
Theorem	elima3 5016*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.)
|- A e. _V   =>    |- ( A e. ( B " C ) <-> E. x ( x e. C /\ <. x , A >. e. B ) )
Theorem	nfima 5017	Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A " B )
Theorem	nfimad 5018	Deduction version of bound-variable hypothesis builder nfima 5017. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x ( A " B ) )
Theorem	imadmrn 5019	The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.)
|- ( A " dom A ) = ran A
Theorem	imassrn 5020	The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.)
|- ( A " B ) C_ ran A
Theorem	mptima 5021*	Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ( x e. A |-> B ) " C ) = ran ( x e. ( A i^i C ) |-> B )
Theorem	mptimass 5022*	Image of a function in maps-to notation for a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> C C_ A )   =>    |- ( ph -> ( ( x e. A |-> B ) " C ) = ran ( x e. C |-> B ) )
Theorem	imaexg 5023	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 5024	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	imai 5025	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.)
|- ( _I " A ) = A
Theorem	rnresi 5026	The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
|- ran ( _I |` A ) = A
Theorem	resiima 5027	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
|- ( B C_ A -> ( ( _I |` A ) " B ) = B )
Theorem	ima0 5028	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
|- ( A " (/) ) = (/)
Theorem	0ima 5029	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
|- ( (/) " A ) = (/)
Theorem	csbima12g 5030	Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)
|- ( A e. C -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )
Theorem	imadisj 5031	A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.)
|- ( ( A " B ) = (/) <-> ( dom A i^i B ) = (/) )
Theorem	cnvimass 5032	A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)
|- ( `' A " B ) C_ dom A
Theorem	cnvimarndm 5033	The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.)
|- ( `' A " ran A ) = dom A
Theorem	imasng 5034*	The image of a singleton. (Contributed by NM, 8-May-2005.)
|- ( A e. B -> ( R " { A } ) = { y | A R y } )
Theorem	elrelimasn 5035	Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015.)
|- ( Rel R -> ( B e. ( R " { A } ) <-> A R B ) )
Theorem	elimasn 5036	Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- B e. _V   &    |- C e. _V   =>    |- ( C e. ( A " { B } ) <-> <. B , C >. e. A )
Theorem	elimasng 5037	Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.)
|- ( ( B e. V /\ C e. W ) -> ( C e. ( A " { B } ) <-> <. B , C >. e. A ) )
Theorem	args 5038*	Two ways to express the class of unique-valued arguments of F, which is the same as the domain of F whenever F is a function. The left-hand side of the equality is from Definition 10.2 of [Quine] p. 65. Quine uses the notation "arg F " for this class (for which we have no separate notation). (Contributed by NM, 8-May-2005.)
|- { x | E. y ( F " { x } ) = { y } } = { x | E! y x F y }
Theorem	eliniseg 5039	Membership in an initial segment. The idiom ( `' A " { B } ), meaning { x | x A B }, is used to specify an initial segment in (for example) Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- C e. _V   =>    |- ( B e. V -> ( C e. ( `' A " { B } ) <-> C A B ) )
Theorem	epini 5040	Any set is equal to its preimage under the converse epsilon relation. (Contributed by Mario Carneiro, 9-Mar-2013.)
|- A e. _V   =>    |- ( `' _E " { A } ) = A
Theorem	iniseg 5041*	An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.)
|- ( B e. V -> ( `' A " { B } ) = { x | x A B } )
Theorem	dfse2 5042*	Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015.)
|- ( R Se A <-> A. x e. A ( A i^i ( `' R " { x } ) ) e. _V )
Theorem	exse2 5043	Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- ( R e. V -> R Se A )
Theorem	imass1 5044	Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
|- ( A C_ B -> ( A " C ) C_ ( B " C ) )
Theorem	imass2 5045	Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> ( C " A ) C_ ( C " B ) )
Theorem	ndmima 5046	The image of a singleton outside the domain is empty. (Contributed by NM, 22-May-1998.)
|- ( -. A e. dom B -> ( B " { A } ) = (/) )
Theorem	relcnv 5047	A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.)
|- Rel `' A
Theorem	relbrcnvg 5048	When R is a relation, the sethood assumptions on brcnv 4849 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- ( Rel R -> ( A `' R B <-> B R A ) )
Theorem	eliniseg2 5049	Eliminate the class existence constraint in eliniseg 5039. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 17-Nov-2015.)
|- ( Rel A -> ( C e. ( `' A " { B } ) <-> C A B ) )
Theorem	relbrcnv 5050	When R is a relation, the sethood assumptions on brcnv 4849 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- Rel R   =>    |- ( A `' R B <-> B R A )
Theorem	cotr 5051*	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( R o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
Theorem	issref 5052*	Two ways to state a relation is reflexive. Adapted from Tarski. (Contributed by FL, 15-Jan-2012.) (Revised by NM, 30-Mar-2016.)
|- ( ( _I |` A ) C_ R <-> A. x e. A x R x )
Theorem	cnvsym 5053*	Two ways of saying a relation is symmetric. Similar to definition of symmetry in [Schechter] p. 51. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )
Theorem	intasym 5054*	Two ways of saying a relation is antisymmetric. Definition of antisymmetry in [Schechter] p. 51. (Contributed by NM, 9-Sep-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( R i^i `' R ) C_ _I <-> A. x A. y ( ( x R y /\ y R x ) -> x = y ) )
Theorem	asymref 5055*	Two ways of saying a relation is antisymmetric and reflexive. U. U. R is the field of a relation by relfld 5198. (Contributed by NM, 6-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( R i^i `' R ) = ( _I |` U. U. R ) <-> A. x e. U. U. R A. y ( ( x R y /\ y R x ) <-> x = y ) )
Theorem	intirr 5056*	Two ways of saying a relation is irreflexive. Definition of irreflexivity in [Schechter] p. 51. (Contributed by NM, 9-Sep-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( R i^i _I ) = (/) <-> A. x -. x R x )
Theorem	brcodir 5057*	Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015.)
|- ( ( A e. V /\ B e. W ) -> ( A ( `' R o. R ) B <-> E. z ( A R z /\ B R z ) ) )
Theorem	codir 5058*	Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013.)
|- ( ( A X. B ) C_ ( `' R o. R ) <-> A. x e. A A. y e. B E. z ( x R z /\ y R z ) )
Theorem	qfto 5059*	A quantifier-free way of expressing the total order predicate. (Contributed by Mario Carneiro, 22-Nov-2013.)
|- ( ( A X. B ) C_ ( R u. `' R ) <-> A. x e. A A. y e. B ( x R y \/ y R x ) )
Theorem	xpidtr 5060	A square cross product ( A X. A ) is a transitive relation. (Contributed by FL, 31-Jul-2009.)
|- ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )
Theorem	trin2 5061	The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.)
|- ( ( ( R o. R ) C_ R /\ ( S o. S ) C_ S ) -> ( ( R i^i S ) o. ( R i^i S ) ) C_ ( R i^i S ) )
Theorem	poirr2 5062	A partial order relation is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.)
|- ( R Po A -> ( R i^i ( _I |` A ) ) = (/) )
Theorem	trinxp 5063	The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a square cross product is a way to restrict it to a subset of its field.) (Contributed by FL, 31-Jul-2009.)
|- ( ( R o. R ) C_ R -> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ ( R i^i ( A X. A ) ) )
Theorem	soirri 5064	A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- -. A R A
Theorem	sotri 5065	A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- ( ( A R B /\ B R C ) -> A R C )
Theorem	son2lpi 5066	A strict order relation has no 2-cycle loops. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- -. ( A R B /\ B R A )
Theorem	sotri2 5067	A transitivity relation. (Read -. B < A and B < C implies A < C .) (Contributed by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- ( ( A e. S /\ -. B R A /\ B R C ) -> A R C )
Theorem	sotri3 5068	A transitivity relation. (Read A < B and -. C < B implies A < C .) (Contributed by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- ( ( C e. S /\ A R B /\ -. C R B ) -> A R C )
Theorem	poleloe 5069	Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( B e. V -> ( A ( R u. _I ) B <-> ( A R B \/ A = B ) ) )
Theorem	poltletr 5070	Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R B /\ B ( R u. _I ) C ) -> A R C ) )
Theorem	cnvopab 5071*	The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' { <. x , y >. | ph } = { <. y , x >. | ph }
Theorem	mptcnv 5072*	The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.)
|- ( ph -> ( ( x e. A /\ y = B ) <-> ( y e. C /\ x = D ) ) )   =>    |- ( ph -> `' ( x e. A |-> B ) = ( y e. C |-> D ) )
Theorem	cnv0 5073	The converse of the empty set. (Contributed by NM, 6-Apr-1998.)
|- `' (/) = (/)
Theorem	cnvi 5074	The converse of the identity relation. Theorem 3.7(ii) of [Monk1] p. 36. (Contributed by NM, 26-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' _I = _I
Theorem	cnvun 5075	The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' ( A u. B ) = ( `' A u. `' B )
Theorem	cnvdif 5076	Distributive law for converse over set difference. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- `' ( A \ B ) = ( `' A \ `' B )
Theorem	cnvin 5077	Distributive law for converse over intersection. Theorem 15 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Revised by Mario Carneiro, 26-Jun-2014.)
|- `' ( A i^i B ) = ( `' A i^i `' B )
Theorem	rnun 5078	Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.)
|- ran ( A u. B ) = ( ran A u. ran B )
Theorem	rnin 5079	The range of an intersection belongs the intersection of ranges. Theorem 9 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.)
|- ran ( A i^i B ) C_ ( ran A i^i ran B )
Theorem	rniun 5080	The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
|- ran U_ x e. A B = U_ x e. A ran B
Theorem	rnuni 5081*	The range of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 17-Mar-2004.) (Revised by Mario Carneiro, 29-May-2015.)
|- ran U. A = U_ x e. A ran x
Theorem	imaundi 5082	Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
|- ( A " ( B u. C ) ) = ( ( A " B ) u. ( A " C ) )
Theorem	imaundir 5083	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|- ( ( A u. B ) " C ) = ( ( A " C ) u. ( B " C ) )
Theorem	dminss 5084	An upper bound for intersection with a domain. Theorem 40 of [Suppes] p. 66, who calls it "somewhat surprising". (Contributed by NM, 11-Aug-2004.)
|- ( dom R i^i A ) C_ ( `' R " ( R " A ) )
Theorem	imainss 5085	An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by NM, 11-Aug-2004.)
|- ( ( R " A ) i^i B ) C_ ( R " ( A i^i ( `' R " B ) ) )
Theorem	inimass 5086	The image of an intersection. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i B ) " C ) C_ ( ( A " C ) i^i ( B " C ) )
Theorem	inimasn 5087	The intersection of the image of singleton. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( C e. V -> ( ( A i^i B ) " { C } ) = ( ( A " { C } ) i^i ( B " { C } ) ) )
Theorem	cnvxp 5088	The converse of a cross product. Exercise 11 of [Suppes] p. 67. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' ( A X. B ) = ( B X. A )
Theorem	xp0 5089	The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.)
|- ( A X. (/) ) = (/)
Theorem	xpmlem 5090*	The cross product of inhabited classes is inhabited. (Contributed by Jim Kingdon, 11-Dec-2018.)
|- ( ( E. x x e. A /\ E. y y e. B ) <-> E. z z e. ( A X. B ) )
Theorem	xpm 5091*	The cross product of inhabited classes is inhabited. (Contributed by Jim Kingdon, 13-Dec-2018.)
|- ( ( E. x x e. A /\ E. y y e. B ) <-> E. z z e. ( A X. B ) )
Theorem	xpeq0r 5092	A cross product is empty if at least one member is empty. (Contributed by Jim Kingdon, 12-Dec-2018.)
|- ( ( A = (/) \/ B = (/) ) -> ( A X. B ) = (/) )
Theorem	sqxpeq0 5093	A Cartesian square is empty iff its member is empty. (Contributed by Jim Kingdon, 21-Apr-2023.)
|- ( ( A X. A ) = (/) <-> A = (/) )
Theorem	xpdisj1 5094	Cross products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.)
|- ( ( A i^i B ) = (/) -> ( ( A X. C ) i^i ( B X. D ) ) = (/) )
Theorem	xpdisj2 5095	Cross products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.)
|- ( ( A i^i B ) = (/) -> ( ( C X. A ) i^i ( D X. B ) ) = (/) )
Theorem	xpsndisj 5096	Cross products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004.)
|- ( B =/= D -> ( ( A X. { B } ) i^i ( C X. { D } ) ) = (/) )
Theorem	djudisj 5097*	Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|- ( ( A i^i B ) = (/) -> ( U_ x e. A ( { x } X. C ) i^i U_ y e. B ( { y } X. D ) ) = (/) )
Theorem	resdisj 5098	A double restriction to disjoint classes is the empty set. (Contributed by NM, 7-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A i^i B ) = (/) -> ( ( C |` A ) |` B ) = (/) )
Theorem	rnxpm 5099*	The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37, with nonempty changed to inhabited. (Contributed by Jim Kingdon, 12-Dec-2018.)
|- ( E. x x e. A -> ran ( A X. B ) = B )
Theorem	dmxpss 5100	The domain of a cross product is a subclass of the first factor. (Contributed by NM, 19-Mar-2007.)
|- dom ( A X. B ) C_ A