P. 53 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5201-5300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	resiima 5201	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
|- ( B C_ A -> ( ( _I |` A ) " B ) = B )
Theorem	ima0 5202	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
|- ( A " (/) ) = (/)
Theorem	0ima 5203	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
|- ( (/) " A ) = (/)
Theorem	csbima12 5204	Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006.) (Revised by NM, 20-Aug-2018.)
|- [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B )
Theorem	csbima12gOLD 5205	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.) Obsolete as of 20-Aug-2018. Use csbfv12 5923 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. C -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )
Theorem	imadisj 5206	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 5207	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 5208	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 5209*	The image of a singleton. (Contributed by NM, 8-May-2005.)
|- ( A e. B -> ( R " { A } ) = { y | A R y } )
Theorem	relimasn 5210*	The image of a singleton. (Contributed by NM, 20-May-1998.)
|- ( Rel R -> ( R " { A } ) = { y | A R y } )
Theorem	elrelimasn 5211	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 5212	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 5213	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	elimasni 5214	Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010.)
|- ( C e. ( A " { B } ) -> B A C )
Theorem	args 5215*	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). Observe the resemblance to the alternate definition dffv4 5885 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005.)
|- { x | E. y ( F " { x } ) = { y } } = { x | E! y x F y }
Theorem	eliniseg 5216	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 5217	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 5218*	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	inisegn0 5219	Nonemptyness of an initial segment in terms of range. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- ( A e. ran F <-> ( `' F " { A } ) =/= (/) )
Theorem	dffr3 5220*	Alternate definition of well-founded relation. Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 23-Apr-2004.) (Revised by Mario Carneiro, 23-Jun-2015.)
|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
Theorem	dfse2 5221*	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	imass1 5222	Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
|- ( A C_ B -> ( A " C ) C_ ( B " C ) )
Theorem	imass2 5223	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 5224	The image of a singleton outside the domain is empty. (Contributed by NM, 22-May-1998.) (Proof shortened by OpenAI, 3-Jul-2020.)
|- ( -. A e. dom B -> ( B " { A } ) = (/) )
Theorem	ndmimaOLD 5225	The image of a singleton outside the domain is empty. (Contributed by NM, 22-May-1998.) Obsolete version of ndmima 5224 as of 3-Jul-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( -. A e. dom B -> ( B " { A } ) = (/) )
Theorem	relcnv 5226	A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.)
|- Rel `' A
Theorem	relbrcnvg 5227	When R is a relation, the sethood assumptions on brcnv 5036 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- ( Rel R -> ( A `' R B <-> B R A ) )
Theorem	eliniseg2 5228	Eliminate the class existence constraint in eliniseg 5216. (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 5229	When R is a relation, the sethood assumptions on brcnv 5036 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- Rel R   =>    |- ( A `' R B <-> B R A )
Theorem	cotrg 5230*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 5231 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 5231. (Revised by Richard Penner, 24-Dec-2019.)
|- ( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) )
Theorem	cotr 5231*	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. Special instance of cotrg 5230. (Contributed by NM, 27-Dec-1996.)
|- ( ( R o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
Theorem	issref 5232*	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 5233*	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 5234*	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 5235*	Two ways of saying a relation is antisymmetric and reflexive. U. U. R is the field of a relation by relfld 5380. (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	asymref2 5236*	Two ways of saying a relation is antisymmetric and reflexive. (Contributed by NM, 6-May-2008.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)
|- ( ( R i^i `' R ) = ( _I |` U. U. R ) <-> ( A. x e. U. U. R x R x /\ A. x A. y ( ( x R y /\ y R x ) -> x = y ) ) )
Theorem	intirr 5237*	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 5238*	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 5239*	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 5240*	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 5241	A square Cartesian 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 5242	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 5243	A partial order relation is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.)
|- ( R Po A -> ( R i^i ( _I |` A ) ) = (/) )
Theorem	trinxp 5244	The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a square Cartesian 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 5245	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 5246	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 5247	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 5248	A transitivity relation. (Read A <_ B 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 5249	A transitivity relation. (Read A < B and B <_ C 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 5250	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 5251	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	somin1 5252	Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( A R B , A , B ) ( R u. _I ) A )
Theorem	somincom 5253	Commutativity of minimum in a total order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( A R B , A , B ) = if ( B R A , B , A ) )
Theorem	somin2 5254	Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( A R B , A , B ) ( R u. _I ) B )
Theorem	soltmin 5255	Being less than a minimum, for a general total order. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A R if ( B R C , B , C ) <-> ( A R B /\ A R C ) ) )
Theorem	cnvopab 5256*	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 5257*	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 5258	The converse of the empty set. (Contributed by NM, 6-Apr-1998.)
|- `' (/) = (/)
Theorem	cnvi 5259	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 5260	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 5261	Distributive law for converse over class difference. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- `' ( A \ B ) = ( `' A \ `' B )
Theorem	cnvin 5262	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 5263	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 5264	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 5265	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 5266*	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 5267	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 5268	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|- ( ( A u. B ) " C ) = ( ( A " C ) u. ( B " C ) )
Theorem	dminss 5269	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 5270	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 5271	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 5272	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 5273	The converse of a Cartesian 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 5274	The Cartesian 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	xpnz 5275	The Cartesian product of nonempty classes is nonempty. (Variation of a theorem contributed by Raph Levien, 30-Jun-2006.) (Contributed by NM, 30-Jun-2006.)
|- ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
Theorem	xpeq0 5276	At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006.)
|- ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )
Theorem	xpdisj1 5277	Cartesian 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 5278	Cartesian 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 5279	Cartesian products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004.)
|- ( B =/= D -> ( ( A X. { B } ) i^i ( C X. { D } ) ) = (/) )
Theorem	difxp 5280	Difference of Cartesian products, expressed in terms of a union of Cartesian products of differences. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 26-Jun-2014.)
|- ( ( C X. D ) \ ( A X. B ) ) = ( ( ( C \ A ) X. D ) u. ( C X. ( D \ B ) ) )
Theorem	difxp1 5281	Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.)
|- ( ( A \ B ) X. C ) = ( ( A X. C ) \ ( B X. C ) )
Theorem	difxp2 5282	Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.)
|- ( A X. ( B \ C ) ) = ( ( A X. B ) \ ( A X. C ) )
Theorem	djudisj 5283*	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	xpdifid 5284*	The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019.)
|- U_ x e. A ( { x } X. ( B \ { x } ) ) = ( ( A X. B ) \ _I )
Theorem	resdisj 5285	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	rnxp 5286	The range of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.)
|- ( A =/= (/) -> ran ( A X. B ) = B )
Theorem	dmxpss 5287	The domain of a Cartesian product is a subclass of the first factor. (Contributed by NM, 19-Mar-2007.)
|- dom ( A X. B ) C_ A
Theorem	rnxpss 5288	The range of a Cartesian product is a subclass of the second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ran ( A X. B ) C_ B
Theorem	rnxpid 5289	The range of a square Cartesian product. (Contributed by FL, 17-May-2010.)
|- ran ( A X. A ) = A
Theorem	ssxpb 5290	A Cartesian product subclass relationship is equivalent to the relationship for it components. (Contributed by NM, 17-Dec-2008.)
|- ( ( A X. B ) =/= (/) -> ( ( A X. B ) C_ ( C X. D ) <-> ( A C_ C /\ B C_ D ) ) )
Theorem	xp11 5291	The Cartesian product of nonempty classes is one-to-one. (Contributed by NM, 31-May-2008.)
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A X. B ) = ( C X. D ) <-> ( A = C /\ B = D ) ) )
Theorem	xpcan 5292	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
|- ( C =/= (/) -> ( ( C X. A ) = ( C X. B ) <-> A = B ) )
Theorem	xpcan2 5293	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
|- ( C =/= (/) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )
Theorem	ssrnres 5294	Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.)
|- ( B C_ ran ( C |` A ) <-> ran ( C i^i ( A X. B ) ) = B )
Theorem	rninxp 5295*	Range of the intersection with a Cartesian product. (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ran ( C i^i ( A X. B ) ) = B <-> A. y e. B E. x e. A x C y )
Theorem	dminxp 5296*	Domain of the intersection with a Cartesian product. (Contributed by NM, 17-Jan-2006.)
|- ( dom ( C i^i ( A X. B ) ) = A <-> A. x e. A E. y e. B x C y )
Theorem	imainrect 5297	Image of a relation restricted to a rectangular region. (Contributed by Stefan O'Rear, 19-Feb-2015.)
|- ( ( G i^i ( A X. B ) ) " Y ) = ( ( G " ( Y i^i A ) ) i^i B )
Theorem	xpima 5298	The image by a constant function (or other Cartesian product). (Contributed by Thierry Arnoux, 4-Feb-2017.)
|- ( ( A X. B ) " C ) = if ( ( A i^i C ) = (/) , (/) , B )
Theorem	xpima1 5299	The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i C ) = (/) -> ( ( A X. B ) " C ) = (/) )
Theorem	xpima2 5300	The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i C ) =/= (/) -> ( ( A X. B ) " C ) = B )