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	rnun 5201	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 5202	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 5203	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 5204*	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 5205	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 5206	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|- ( ( A u. B ) " C ) = ( ( A " C ) u. ( B " C ) )
Theorem	dminss 5207	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 5208	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 5209	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 5210	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 5211	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 5212	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 5213	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 5214	At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006.)
|- ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )
Theorem	xpdisj1 5215	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 5216	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 5217	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 5218	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 5219	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 5220	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 5221*	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 5222*	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 5223	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 5224	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 5225	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 5226	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 5227	The range of a square Cartesian product. (Contributed by FL, 17-May-2010.)
|- ran ( A X. A ) = A
Theorem	ssxpb 5228	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 5229	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 5230	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
|- ( C =/= (/) -> ( ( C X. A ) = ( C X. B ) <-> A = B ) )
Theorem	xpcan2 5231	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
|- ( C =/= (/) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )
Theorem	ssrnres 5232	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 5233*	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 5234*	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 5235	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 5236	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 5237	The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i C ) = (/) -> ( ( A X. B ) " C ) = (/) )
Theorem	xpima2 5238	The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i C ) =/= (/) -> ( ( A X. B ) " C ) = B )
Theorem	xpimasn 5239	The image of a singleton by a Cartesian product. (Contributed by Thierry Arnoux, 14-Jan-2018.) (Proof shortened by BJ, 6-Apr-2019.)
|- ( X e. A -> ( ( A X. B ) " { X } ) = B )
Theorem	sossfld 5240	The base set of a strict order is contained in the field of the relation, except possibly for one element (note that (/) Or { B }). (Contributed by Mario Carneiro, 27-Apr-2015.)
|- ( ( R Or A /\ B e. A ) -> ( A \ { B } ) C_ ( dom R u. ran R ) )
Theorem	sofld 5241	The base set of a nonempty strict order is the same as the field of the relation. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( R Or A /\ R C_ ( A X. A ) /\ R =/= (/) ) -> A = ( dom R u. ran R ) )
Theorem	cnvcnv3 5242*	The set of all ordered pairs in a class is the same as the double converse. (Contributed by Mario Carneiro, 16-Aug-2015.)
|- `' `' R = { <. x , y >. | x R y }
Theorem	dfrel2 5243	Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)
|- ( Rel R <-> `' `' R = R )
Theorem	dfrel4v 5244*	A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 5865 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.)
|- ( Rel R <-> R = { <. x , y >. | x R y } )
Theorem	cnvcnv 5245	The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.)
|- `' `' A = ( A i^i ( _V X. _V ) )
Theorem	cnvcnv2 5246	The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.)
|- `' `' A = ( A |` _V )
Theorem	cnvcnvss 5247	The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.)
|- `' `' A C_ A
Theorem	cnveqb 5248	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
|- ( ( Rel A /\ Rel B ) -> ( A = B <-> `' A = `' B ) )
Theorem	cnveq0 5249	A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.)
|- ( Rel A -> ( A = (/) <-> `' A = (/) ) )
Theorem	dfrel3 5250	Alternate definition of relation. (Contributed by NM, 14-May-2008.)
|- ( Rel R <-> ( R |` _V ) = R )
Theorem	dmresv 5251	The domain of a universal restriction. (Contributed by NM, 14-May-2008.)
|- dom ( A |` _V ) = dom A
Theorem	rnresv 5252	The range of a universal restriction. (Contributed by NM, 14-May-2008.)
|- ran ( A |` _V ) = ran A
Theorem	dfrn4 5253	Range defined in terms of image. (Contributed by NM, 14-May-2008.)
|- ran A = ( A " _V )
Theorem	csbrn 5254	Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
|- [_ A / x ]_ ran B = ran [_ A / x ]_ B
Theorem	rescnvcnv 5255	The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( `' `' A |` B ) = ( A |` B )
Theorem	cnvcnvres 5256	The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.)
|- `' `' ( A |` B ) = ( `' `' A |` B )
Theorem	imacnvcnv 5257	The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
|- ( `' `' A " B ) = ( A " B )
Theorem	dmsnn0 5258	The domain of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A e. ( _V X. _V ) <-> dom { A } =/= (/) )
Theorem	rnsnn0 5259	The range of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008.)
|- ( A e. ( _V X. _V ) <-> ran { A } =/= (/) )
Theorem	dmsn0 5260	The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.)
|- dom { (/) } = (/)
Theorem	cnvsn0 5261	The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- `' { (/) } = (/)
Theorem	dmsn0el 5262	The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008.)
|- ( (/) e. A -> dom { A } = (/) )
Theorem	relsn2 5263	A singleton is a relation iff it has a nonempty domain. (Contributed by NM, 25-Sep-2013.)
|- A e. _V   =>    |- ( Rel { A } <-> dom { A } =/= (/) )
Theorem	dmsnopg 5264	The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( B e. V -> dom { <. A , B >. } = { A } )
Theorem	dmsnopss 5265	The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on B). (Contributed by Mario Carneiro, 30-Apr-2015.)
|- dom { <. A , B >. } C_ { A }
Theorem	dmpropg 5266	The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( B e. V /\ D e. W ) -> dom { <. A , B >. , <. C , D >. } = { A , C } )
Theorem	dmsnop 5267	The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- B e. _V   =>    |- dom { <. A , B >. } = { A }
Theorem	dmprop 5268	The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.)
|- B e. _V   &    |- D e. _V   =>    |- dom { <. A , B >. , <. C , D >. } = { A , C }
Theorem	dmtpop 5269	The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
|- B e. _V   &    |- D e. _V   &    |- F e. _V   =>    |- dom { <. A , B >. , <. C , D >. , <. E , F >. } = { A , C , E }
Theorem	cnvcnvsn 5270	Double converse of a singleton of an ordered pair. (Unlike cnvsn 5276, this does not need any sethood assumptions on A and B.) (Contributed by Mario Carneiro, 26-Apr-2015.)
|- `' `' { <. A , B >. } = `' { <. B , A >. }
Theorem	dmsnsnsn 5271	The domain of the singleton of the singleton of a singleton. (Contributed by NM, 15-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- dom { { { A } } } = { A }
Theorem	rnsnopg 5272	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( A e. V -> ran { <. A , B >. } = { B } )
Theorem	rnpropg 5273	The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
|- ( ( A e. V /\ B e. W ) -> ran { <. A , C >. , <. B , D >. } = { C , D } )
Theorem	rnsnop 5274	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   =>    |- ran { <. A , B >. } = { B }
Theorem	op1sta 5275	Extract the first member of an ordered pair. (See op2nda 5278 to extract the second member, op1stb 4629 for an alternate version, and op1st 6754 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- U. dom { <. A , B >. } = A
Theorem	cnvsn 5276	Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- `' { <. A , B >. } = { <. B , A >. }
Theorem	op2ndb 5277	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 4629 to extract the first member, op2nda 5278 for an alternate version, and op2nd 6755 for the preferred version.) (Contributed by NM, 25-Nov-2003.)
|- A e. _V   &    |- B e. _V   =>    |- |^| |^| |^| `' { <. A , B >. } = B
Theorem	op2nda 5278	Extract the second member of an ordered pair. (See op1sta 5275 to extract the first member, op2ndb 5277 for an alternate version, and op2nd 6755 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- A e. _V   &    |- B e. _V   =>    |- U. ran { <. A , B >. } = B
Theorem	cnvsng 5279	Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.)
|- ( ( A e. V /\ B e. W ) -> `' { <. A , B >. } = { <. B , A >. } )
Theorem	opswap 5280	Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- U. `' { <. A , B >. } = <. B , A >.
Theorem	cnvresima 5281	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
|- ( `' ( F |` A ) " B ) = ( ( `' F " B ) i^i A )
Theorem	resdm2 5282	A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.)
|- ( A |` dom A ) = `' `' A
Theorem	resdmres 5283	Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
|- ( A |` dom ( A |` B ) ) = ( A |` B )
Theorem	imadmres 5284	The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
|- ( A " dom ( A |` B ) ) = ( A " B )
Theorem	mptpreima 5285*	The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- F = ( x e. A |-> B )   =>    |- ( `' F " C ) = { x e. A | B e. C }
Theorem	mptiniseg 5286*	Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- F = ( x e. A |-> B )   =>    |- ( C e. V -> ( `' F " { C } ) = { x e. A | B = C } )
Theorem	dmmpt 5287	The domain of the mapping operation in general. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.)
|- F = ( x e. A |-> B )   =>    |- dom F = { x e. A | B e. _V }
Theorem	dmmptss 5288*	The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
|- F = ( x e. A |-> B )   =>    |- dom F C_ A
Theorem	dmmptg 5289*	The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.)
|- ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )
Theorem	relco 5290	A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)
|- Rel ( A o. B )
Theorem	dfco2 5291*	Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.)
|- ( A o. B ) = U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) )
Theorem	dfco2a 5292*	Generalization of dfco2 5291, where C can have any value between dom A i^i ran B and _V. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( dom A i^i ran B ) C_ C -> ( A o. B ) = U_ x e. C ( ( `' B " { x } ) X. ( A " { x } ) ) )
Theorem	coundi 5293	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A o. ( B u. C ) ) = ( ( A o. B ) u. ( A o. C ) )
Theorem	coundir 5294	Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A u. B ) o. C ) = ( ( A o. C ) u. ( B o. C ) )
Theorem	cores 5295	Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ran B C_ C -> ( ( A |` C ) o. B ) = ( A o. B ) )
Theorem	resco 5296	Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
|- ( ( A o. B ) |` C ) = ( A o. ( B |` C ) )
Theorem	imaco 5297	Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.)
|- ( ( A o. B ) " C ) = ( A " ( B " C ) )
Theorem	rnco 5298	The range of the composition of two classes. (Contributed by NM, 12-Dec-2006.)
|- ran ( A o. B ) = ran ( A |` ran B )
Theorem	rnco2 5299	The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.)
|- ran ( A o. B ) = ( A " ran B )
Theorem	dmco 5300	The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.)
|- dom ( A o. B ) = ( `' B " dom A )