P. 50 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4901-5000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	relopab 4901	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 4902	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 4903	The maps-to notation always describes a relationship. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Rel ( x e. A |-> B )
Theorem	reli 4904	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 4905	The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- Rel _E
Theorem	opabid2 4906*	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 4907*	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 4908*	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 4909	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 4910	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 4911	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 4912*	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 4913*	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 4914*	Membership in a union of cross products. Analogue of elxp 4786 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 4915*	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 4916*	Write a double restricted quantification as one universal quantifier. In this version of ralxp 4918, 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 4917*	Write a double restricted quantification as one universal quantifier. In this version of rexxp 4919, 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 4918*	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 4919*	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 4920*	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 4921*	Version of ralxp 4918 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 4922*	Version of rexxp 4919 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 4923*	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 4924*	Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2359. (Contributed by NM, 24-Feb-2014.)
|- Rel A   &    |- ( ph -> ( <. x , y >. e. A <-> ps ) )   =>    |- ( ph -> A = { <. x , y >. | ps } )
Theorem	relop 4925*	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 4926	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 4927	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 4928	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 4929	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 4930	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|- ( A C_ B -> ( A o. C ) C_ ( B o. C ) )
Theorem	coss2 4931	Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|- ( A C_ B -> ( C o. A ) C_ ( C o. B ) )
Theorem	coeq1 4932	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- ( A = B -> ( A o. C ) = ( B o. C ) )
Theorem	coeq2 4933	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- ( A = B -> ( C o. A ) = ( C o. B ) )
Theorem	coeq1i 4934	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>    |- ( A o. C ) = ( B o. C )
Theorem	coeq2i 4935	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>    |- ( C o. A ) = ( C o. B )
Theorem	coeq1d 4936	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 4937	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 4938	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 4939	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 4940	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 4941*	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 4942*	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 4943*	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 4944	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 4945*	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 4946*	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 4947*	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 4948	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> `' A C_ `' B )
Theorem	cnveq 4949	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|- ( A = B -> `' A = `' B )
Theorem	cnveqi 4950	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|- A = B   =>    |- `' A = `' B
Theorem	cnveqd 4951	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> `' A = `' B )
Theorem	elcnv 4952*	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 4953*	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 4954	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 4955	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 4956	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 4957	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 4958	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 4959	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 4960	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 4961*	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 4962*	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 4963*	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 4964*	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 4965*	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 4966*	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 4967*	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 4968	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|- dom A = ran `' A
Theorem	dfdmf 4969*	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 4970	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 4971*	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 4972*	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 4973*	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 4974*	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 4975	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A C_ B -> dom A C_ dom B )
Theorem	dmeq 4976	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A = B -> dom A = dom B )
Theorem	dmeqi 4977	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- dom A = dom B
Theorem	dmeqd 4978	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> dom A = dom B )
Theorem	opeldm 4979	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 4980	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 4981	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 4982	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 4983	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 4984	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 )
Theorem	dmiun 4985	The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- dom U_ x e. A B = U_ x e. A dom B
Theorem	dmuni 4986*	The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.)
|- dom U. A = U_ x e. A dom x
Theorem	dmopab 4987*	The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|- dom { <. x , y >. | ph } = { x | E. y ph }
Theorem	dmopabss 4988*	Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
|- dom { <. x , y >. | ( x e. A /\ ph ) } C_ A
Theorem	dmopab3 4989*	The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
|- ( A. x e. A E. y ph <-> dom { <. x , y >. | ( x e. A /\ ph ) } = A )
Theorem	dm0 4990	The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- dom (/) = (/)
Theorem	dmi 4991	The domain of the identity relation is the universe. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- dom _I = _V
Theorem	dmv 4992	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
|- dom _V = _V
Theorem	dm0rn0 4993	An empty domain implies an empty range. For a similar theorem for whether the domain and range are inhabited, see dmmrnm 4996. (Contributed by NM, 21-May-1998.)
|- ( dom A = (/) <-> ran A = (/) )
Theorem	reldm0 4994	A relation is empty iff its domain is empty. For a similar theorem for whether the relation and domain are inhabited, see reldmm 4995. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> dom A = (/) ) )
Theorem	reldmm 4995*	A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.)
|- ( Rel A -> ( E. x x e. A <-> E. y y e. dom A ) )
Theorem	dmmrnm 4996*	A domain is inhabited if and only if the range is inhabited. (Contributed by Jim Kingdon, 15-Dec-2018.)
|- ( E. x x e. dom A <-> E. y y e. ran A )
Theorem	dmxpm 4997*	The domain of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( E. x x e. B -> dom ( A X. B ) = A )
Theorem	dmxpid 4998	The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.) (Revised by Jim Kingdon, 11-Apr-2023.)
|- dom ( A X. A ) = A
Theorem	dmxpin 4999	The domain of the intersection of two square Cartesian products. Unlike dmin 4984, equality holds. (Contributed by NM, 29-Jan-2008.)
|- dom ( ( A X. A ) i^i ( B X. B ) ) = ( A i^i B )
Theorem	xpid11 5000	The Cartesian product of a class with itself is one-to-one. (Contributed by NM, 5-Nov-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A X. A ) = ( B X. B ) <-> A = B )