P. 49 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4801-4900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unixpss 4801	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 4802	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 4803	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 4804	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 4805	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 4806	The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994.)
|- ( Rel A -> Rel ( A i^i B ) )
Theorem	relin2 4807	The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006.)
|- ( Rel B -> Rel ( A i^i B ) )
Theorem	reldif 4808	A difference cutting down a relation is a relation. (Contributed by NM, 31-Mar-1998.)
|- ( Rel A -> Rel ( A \ B ) )
Theorem	reliun 4809	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 )
Theorem	reliin 4810	An indexed intersection is a relation if at least one of the member of the indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
|- ( E. x e. A Rel B -> Rel |^|_ x e. A B )
Theorem	reluni 4811*	The union of a class is a relation iff any member is a relation. Exercise 6 of [TakeutiZaring] p. 25 and its converse. (Contributed by NM, 13-Aug-2004.)
|- ( Rel U. A <-> A. x e. A Rel x )
Theorem	relint 4812*	The intersection of a class is a relation if at least one member is a relation. (Contributed by NM, 8-Mar-2014.)
|- ( E. x e. A Rel x -> Rel |^| A )
Theorem	rel0 4813	The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
|- Rel (/)
Theorem	relopabiv 4814*	A class of ordered pairs is a relation. For a version without a disjoint variable condition, see relopabi 4816. (Contributed by BJ, 22-Jul-2023.)
|- A = { <. x , y >. | ph }   =>    |- Rel A
Theorem	relopabv 4815*	A class of ordered pairs is a relation. For a version without a disjoint variable condition, see relopab 4817. (Contributed by SN, 8-Sep-2024.)
|- Rel { <. x , y >. | ph }
Theorem	relopabi 4816	A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.)
|- A = { <. x , y >. | ph }   =>    |- Rel A
Theorem	relopab 4817	A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) (Unnecessary distinct variable restrictions were removed by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
|- Rel { <. x , y >. | ph }
Theorem	brabv 4818	If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
|- ( X { <. x , y >. | ph } Y -> ( X e. _V /\ Y e. _V ) )
Theorem	mptrel 4819	The maps-to notation always describes a relationship. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Rel ( x e. A |-> B )
Theorem	reli 4820	The identity relation is a relation. Part of Exercise 4.12(p) of [Mendelson] p. 235. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- Rel _I
Theorem	rele 4821	The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- Rel _E
Theorem	opabid2 4822*	A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006.)
|- ( Rel A -> { <. x , y >. | <. x , y >. e. A } = A )
Theorem	inopab 4823*	Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ( { <. x , y >. | ph } i^i { <. x , y >. | ps } ) = { <. x , y >. | ( ph /\ ps ) }
Theorem	difopab 4824*	The difference of two ordered-pair abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) = { <. x , y >. | ( ph /\ -. ps ) }
Theorem	inxp 4825	The intersection of two cross products. Exercise 9 of [TakeutiZaring] p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A X. B ) i^i ( C X. D ) ) = ( ( A i^i C ) X. ( B i^i D ) )
Theorem	xpindi 4826	Distributive law for cross product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
|- ( A X. ( B i^i C ) ) = ( ( A X. B ) i^i ( A X. C ) )
Theorem	xpindir 4827	Distributive law for cross product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
|- ( ( A i^i B ) X. C ) = ( ( A X. C ) i^i ( B X. C ) )
Theorem	xpiindim 4828*	Distributive law for cross product over indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|- ( E. y y e. A -> ( C X. |^|_ x e. A B ) = |^|_ x e. A ( C X. B ) )
Theorem	xpriindim 4829*	Distributive law for cross product over relativized indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|- ( E. y y e. A -> ( C X. ( D i^i |^|_ x e. A B ) ) = ( ( C X. D ) i^i |^|_ x e. A ( C X. B ) ) )
Theorem	eliunxp 4830*	Membership in a union of cross products. Analogue of elxp 4705 for nonconstant B ( x ). (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( C e. U_ x e. A ( { x } X. B ) <-> E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
Theorem	opeliunxp2 4831*	Membership in a union of cross products. (Contributed by Mario Carneiro, 14-Feb-2015.)
|- ( x = C -> B = E )   =>    |- ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )
Theorem	raliunxp 4832*	Write a double restricted quantification as one universal quantifier. In this version of ralxp 4834, B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( A. x e. U_ y e. A ( { y } X. B ) ph <-> A. y e. A A. z e. B ps )
Theorem	rexiunxp 4833*	Write a double restricted quantification as one universal quantifier. In this version of rexxp 4835, B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( E. x e. U_ y e. A ( { y } X. B ) ph <-> E. y e. A E. z e. B ps )
Theorem	ralxp 4834*	Universal quantification restricted to a cross product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )
Theorem	rexxp 4835*	Existential quantification restricted to a cross product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )
Theorem	djussxp 4836*	Disjoint union is a subset of a cross product. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|- U_ x e. A ( { x } X. B ) C_ ( A X. _V )
Theorem	ralxpf 4837*	Version of ralxp 4834 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- F/ z ph   &    |- F/ x ps   &    |- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )
Theorem	rexxpf 4838*	Version of rexxp 4835 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- F/ z ph   &    |- F/ x ps   &    |- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )
Theorem	iunxpf 4839*	Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
|- F/_ y C   &    |- F/_ z C   &    |- F/_ x D   &    |- ( x = <. y , z >. -> C = D )   =>    |- U_ x e. ( A X. B ) C = U_ y e. A U_ z e. B D
Theorem	opabbi2dv 4840*	Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2325. (Contributed by NM, 24-Feb-2014.)
|- Rel A   &    |- ( ph -> ( <. x , y >. e. A <-> ps ) )   =>    |- ( ph -> A = { <. x , y >. | ps } )
Theorem	relop 4841*	A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)
|- A e. _V   &    |- B e. _V   =>    |- ( Rel <. A , B >. <-> E. x E. y ( A = { x } /\ B = { x , y } ) )
Theorem	ideqg 4842	For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( B e. V -> ( A _I B <-> A = B ) )
Theorem	ideq 4843	For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)
|- B e. _V   =>    |- ( A _I B <-> A = B )
Theorem	ididg 4844	A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A e. V -> A _I A )
Theorem	issetid 4845	Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A e. _V <-> A _I A )
Theorem	coss1 4846	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|- ( A C_ B -> ( A o. C ) C_ ( B o. C ) )
Theorem	coss2 4847	Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|- ( A C_ B -> ( C o. A ) C_ ( C o. B ) )
Theorem	coeq1 4848	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- ( A = B -> ( A o. C ) = ( B o. C ) )
Theorem	coeq2 4849	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- ( A = B -> ( C o. A ) = ( C o. B ) )
Theorem	coeq1i 4850	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>    |- ( A o. C ) = ( B o. C )
Theorem	coeq2i 4851	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>    |- ( C o. A ) = ( C o. B )
Theorem	coeq1d 4852	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A o. C ) = ( B o. C ) )
Theorem	coeq2d 4853	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C o. A ) = ( C o. B ) )
Theorem	coeq12i 4854	Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
|- A = B   &    |- C = D   =>    |- ( A o. C ) = ( B o. D )
Theorem	coeq12d 4855	Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A o. C ) = ( B o. D ) )
Theorem	nfco 4856	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A o. B )
Theorem	elco 4857*	Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
|- ( A e. ( R o. S ) <-> E. x E. y E. z ( A = <. x , z >. /\ ( x S y /\ y R z ) ) )
Theorem	brcog 4858*	Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)
|- ( ( A e. V /\ B e. W ) -> ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) ) )
Theorem	opelco2g 4859*	Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. ( C o. D ) <-> E. x ( <. A , x >. e. D /\ <. x , B >. e. C ) ) )
Theorem	brcogw 4860	Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.)
|- ( ( ( A e. V /\ B e. W /\ X e. Z ) /\ ( A D X /\ X C B ) ) -> A ( C o. D ) B )
Theorem	eqbrrdva 4861*	Deduction from extensionality principle for relations, given an equivalence only on the relation's domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.)
|- ( ph -> A C_ ( C X. D ) )   &    |- ( ph -> B C_ ( C X. D ) )   &    |- ( ( ph /\ x e. C /\ y e. D ) -> ( x A y <-> x B y ) )   =>    |- ( ph -> A = B )
Theorem	brco 4862*	Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) )
Theorem	opelco 4863*	Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. ( C o. D ) <-> E. x ( A D x /\ x C B ) )
Theorem	cnvss 4864	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> `' A C_ `' B )
Theorem	cnveq 4865	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|- ( A = B -> `' A = `' B )
Theorem	cnveqi 4866	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|- A = B   =>    |- `' A = `' B
Theorem	cnveqd 4867	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> `' A = `' B )
Theorem	elcnv 4868*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
|- ( A e. `' R <-> E. x E. y ( A = <. x , y >. /\ y R x ) )
Theorem	elcnv2 4869*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
|- ( A e. `' R <-> E. x E. y ( A = <. x , y >. /\ <. y , x >. e. R ) )
Theorem	nfcnv 4870	Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   =>    |- F/_ x `' A
Theorem	opelcnvg 4871	Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. `' R <-> <. B , A >. e. R ) )
Theorem	brcnvg 4872	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
|- ( ( A e. C /\ B e. D ) -> ( A `' R B <-> B R A ) )
Theorem	opelcnv 4873	Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. `' R <-> <. B , A >. e. R )
Theorem	brcnv 4874	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( A `' R B <-> B R A )
Theorem	csbcnvg 4875	Move class substitution in and out of the converse of a function. (Contributed by Thierry Arnoux, 8-Feb-2017.)
|- ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )
Theorem	cnvco 4876	Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' ( A o. B ) = ( `' B o. `' A )
Theorem	cnvuni 4877*	The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
|- `' U. A = U_ x e. A `' x
Theorem	dfdm3 4878*	Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
|- dom A = { x | E. y <. x , y >. e. A }
Theorem	dfrn2 4879*	Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)
|- ran A = { y | E. x x A y }
Theorem	dfrn3 4880*	Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
|- ran A = { y | E. x <. x , y >. e. A }
Theorem	elrn2g 4881*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( A e. V -> ( A e. ran B <-> E. x <. x , A >. e. B ) )
Theorem	elrng 4882*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( A e. V -> ( A e. ran B <-> E. x x B A ) )
Theorem	ssrelrn 4883*	If a relation is a subset of a cartesian product, then for each element of the range of the relation there is an element of the first set of the cartesian product which is related to the element of the range by the relation. (Contributed by AV, 24-Oct-2020.)
|- ( ( R C_ ( A X. B ) /\ Y e. ran R ) -> E. a e. A a R Y )
Theorem	dfdm4 4884	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|- dom A = ran `' A
Theorem	dfdmf 4885*	Definition of domain, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   &    |- F/_ y A   =>    |- dom A = { x | E. y x A y }
Theorem	csbdmg 4886	Distribute proper substitution through the domain of a class. (Contributed by Jim Kingdon, 8-Dec-2018.)
|- ( A e. V -> [_ A / x ]_ dom B = dom [_ A / x ]_ B )
Theorem	eldmg 4887*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> ( A e. dom B <-> E. y A B y ) )
Theorem	eldm2g 4888*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> ( A e. dom B <-> E. y <. A , y >. e. B ) )
Theorem	eldm 4889*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
|- A e. _V   =>    |- ( A e. dom B <-> E. y A B y )
Theorem	eldm2 4890*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)
|- A e. _V   =>    |- ( A e. dom B <-> E. y <. A , y >. e. B )
Theorem	dmss 4891	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A C_ B -> dom A C_ dom B )
Theorem	dmeq 4892	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A = B -> dom A = dom B )
Theorem	dmeqi 4893	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- dom A = dom B
Theorem	dmeqd 4894	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> dom A = dom B )
Theorem	opeldm 4895	Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. C -> A e. dom C )
Theorem	breldm 4896	Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( A R B -> A e. dom R )
Theorem	opeldmg 4897	Membership of first of an ordered pair in a domain. (Contributed by Jim Kingdon, 9-Jul-2019.)
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. C -> A e. dom C ) )
Theorem	breldmg 4898	Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
|- ( ( A e. C /\ B e. D /\ A R B ) -> A e. dom R )
Theorem	dmun 4899	The domain of a union is the union of domains. Exercise 56(a) of [Enderton] p. 65. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- dom ( A u. B ) = ( dom A u. dom B )
Theorem	dmin 4900	The domain of an intersection belong to the intersection of domains. Theorem 6 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.)
|- dom ( A i^i B ) C_ ( dom A i^i dom B )