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	rnresi 5201	The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
|- ran ( _I |` A ) = A
Theorem	resiima 5202	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
|- ( B C_ A -> ( ( _I |` A ) " B ) = B )
Theorem	ima0 5203	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
|- ( A " (/) ) = (/)
Theorem	0ima 5204	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
|- ( (/) " A ) = (/)
Theorem	csbima12 5205	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 5206	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 5916 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. C -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )
Theorem	imadisj 5207	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 5208	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 5209	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 5210*	The image of a singleton. (Contributed by NM, 8-May-2005.)
|- ( A e. B -> ( R " { A } ) = { y | A R y } )
Theorem	relimasn 5211*	The image of a singleton. (Contributed by NM, 20-May-1998.)
|- ( Rel R -> ( R " { A } ) = { y | A R y } )
Theorem	elrelimasn 5212	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 5213	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 5214	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 5215	Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010.)
|- ( C e. ( A " { B } ) -> B A C )
Theorem	args 5216*	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 alternative definition dffv4 5878 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 5217	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 5218	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 5219*	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 5220	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 5221*	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 5222*	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 5223	Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
|- ( A C_ B -> ( A " C ) C_ ( B " C ) )
Theorem	imass2 5224	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 5225	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 5226	The image of a singleton outside the domain is empty. (Contributed by NM, 22-May-1998.) Obsolete version of ndmima 5225 as of 3-Jul-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( -. A e. dom B -> ( B " { A } ) = (/) )
Theorem	relcnv 5227	A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.)
|- Rel `' A
Theorem	relbrcnvg 5228	When R is a relation, the sethood assumptions on brcnv 5037 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- ( Rel R -> ( A `' R B <-> B R A ) )
Theorem	eliniseg2 5229	Eliminate the class existence constraint in eliniseg 5217. (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 5230	When R is a relation, the sethood assumptions on brcnv 5037 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- Rel R   =>    |- ( A `' R B <-> B R A )
Theorem	cotrg 5231*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 5232 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 5232. (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 5232*	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. Special instance of cotrg 5231. (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 5233*	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 5234*	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 5235*	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 5236*	Two ways of saying a relation is antisymmetric and reflexive. U. U. R is the field of a relation by relfld 5381. (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 5237*	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 5238*	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 5239*	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 5240*	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 5241*	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 5242	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 5243	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 5244	A partial order relation is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.)
|- ( R Po A -> ( R i^i ( _I |` A ) ) = (/) )
Theorem	trinxp 5245	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 5246	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 5247	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 5248	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 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 )   =>    |- ( ( A e. S /\ -. B R A /\ B R C ) -> A R C )
Theorem	sotri3 5250	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 5251	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 5252	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 5253	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 5254	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 5255	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 5256	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 5257*	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 5258*	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 5259	The converse of the empty set. (Contributed by NM, 6-Apr-1998.)
|- `' (/) = (/)
Theorem	cnvi 5260	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 5261	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 5262	Distributive law for converse over set difference. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- `' ( A \ B ) = ( `' A \ `' B )
Theorem	cnvin 5263	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 5264	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 5265	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 5266	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 5267*	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 5268	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 5269	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|- ( ( A u. B ) " C ) = ( ( A " C ) u. ( B " C ) )
Theorem	dminss 5270	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 5271	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 5272	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 5273	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 5274	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 5275	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 5276	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 5277	At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006.)
|- ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )
Theorem	xpdisj1 5278	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 5279	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 5280	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 5281	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 5282	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 5283	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 5284*	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 5285*	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 5286	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 5287	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 5288	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 5289	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 5290	The range of a square Cartesian product. (Contributed by FL, 17-May-2010.)
|- ran ( A X. A ) = A
Theorem	ssxpb 5291	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 5292	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 5293	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
|- ( C =/= (/) -> ( ( C X. A ) = ( C X. B ) <-> A = B ) )
Theorem	xpcan2 5294	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
|- ( C =/= (/) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )
Theorem	ssrnres 5295	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 5296*	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 5297*	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 5298	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 5299	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 5300	The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i C ) = (/) -> ( ( A X. B ) " C ) = (/) )