P. 56 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5501-5600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imass2 5501	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 5502	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	relcnv 5503	A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.)
|- Rel `' A
Theorem	relbrcnvg 5504	When R is a relation, the sethood assumptions on brcnv 5305 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- ( Rel R -> ( A `' R B <-> B R A ) )
Theorem	eliniseg2 5505	Eliminate the class existence constraint in eliniseg 5494. (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 5506	When R is a relation, the sethood assumptions on brcnv 5305 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- Rel R   =>    |- ( A `' R B <-> B R A )
Theorem	cotrg 5507*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 5508 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 5508. (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 5508*	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. Special instance of cotrg 5507. (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 5509*	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 5510*	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 5511*	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 5512*	Two ways of saying a relation is antisymmetric and reflexive. U. U. R is the field of a relation by relfld 5661. (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 5513*	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 5514*	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 5515*	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 5516*	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 5517*	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 5518	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 5519	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 5520	A partial order relation is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.)
|- ( R Po A -> ( R i^i ( _I |` A ) ) = (/) )
Theorem	trinxp 5521	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 5522	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 5523	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 5524	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 5525	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 5526	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 5527	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 5528	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 5529	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 5530	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 5531	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 5532	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 5533*	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 5534*	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 5535	The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 4781, ax-nul 4789, ax-pr 4906. (Revised by KP, 25-Oct-2021.)
|- `' (/) = (/)
Theorem	cnv0OLD 5536	Obsolete version of cnv0 5535 as of 25-Oct-2021. (Contributed by NM, 6-Apr-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
|- `' (/) = (/)
Theorem	cnvi 5537	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 5538	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 5539	Distributive law for converse over class difference. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- `' ( A \ B ) = ( `' A \ `' B )
Theorem	cnvin 5540	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 5541	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 5542	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 5543	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 5544*	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 5545	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 5546	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|- ( ( A u. B ) " C ) = ( ( A " C ) u. ( B " C ) )
Theorem	dminss 5547	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 5548	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 5549	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 5550	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 5551	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 5552	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 5553	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 5554	At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006.)
|- ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )
Theorem	xpdisj1 5555	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 5556	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 5557	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 5558	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 5559	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 5560	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 5561*	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 5562*	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 5563	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 5564	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 5565	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 5566	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 5567	The range of a square Cartesian product. (Contributed by FL, 17-May-2010.)
|- ran ( A X. A ) = A
Theorem	ssxpb 5568	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 5569	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 5570	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
|- ( C =/= (/) -> ( ( C X. A ) = ( C X. B ) <-> A = B ) )
Theorem	xpcan2 5571	Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.)
|- ( C =/= (/) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )
Theorem	ssrnres 5572	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 5573*	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 5574*	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 5575	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 5576	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 5577	The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i C ) = (/) -> ( ( A X. B ) " C ) = (/) )
Theorem	xpima2 5578	The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i C ) =/= (/) -> ( ( A X. B ) " C ) = B )
Theorem	xpimasn 5579	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 5580	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 5581	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 5582*	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 5583	Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)
|- ( Rel R <-> `' `' R = R )
Theorem	dfrel4v 5584*	A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6241 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.)
|- ( Rel R <-> R = { <. x , y >. | x R y } )
Theorem	dfrel4 5585*	A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6241 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) (Revised by Thierry Arnoux, 11-May-2017.)
|- F/_ x R   &    |- F/_ y R   =>    |- ( Rel R <-> R = { <. x , y >. | x R y } )
Theorem	cnvcnv 5586	The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.) (Proof shortened by BJ, 26-Nov-2021.)
|- `' `' A = ( A i^i ( _V X. _V ) )
Theorem	cnvcnvOLD 5587	Obsolete proof of cnvcnv 5586 as of 26-Nov-2021. (Contributed by NM, 8-Dec-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
|- `' `' A = ( A i^i ( _V X. _V ) )
Theorem	cnvcnv2 5588	The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.)
|- `' `' A = ( A |` _V )
Theorem	cnvcnvss 5589	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 5590	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
|- ( ( Rel A /\ Rel B ) -> ( A = B <-> `' A = `' B ) )
Theorem	cnveq0 5591	A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.)
|- ( Rel A -> ( A = (/) <-> `' A = (/) ) )
Theorem	dfrel3 5592	Alternate definition of relation. (Contributed by NM, 14-May-2008.)
|- ( Rel R <-> ( R |` _V ) = R )
Theorem	dmresv 5593	The domain of a universal restriction. (Contributed by NM, 14-May-2008.)
|- dom ( A |` _V ) = dom A
Theorem	rnresv 5594	The range of a universal restriction. (Contributed by NM, 14-May-2008.)
|- ran ( A |` _V ) = ran A
Theorem	dfrn4 5595	Range defined in terms of image. (Contributed by NM, 14-May-2008.)
|- ran A = ( A " _V )
Theorem	csbrn 5596	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 5597	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 5598	The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.)
|- `' `' ( A |` B ) = ( `' `' A |` B )
Theorem	imacnvcnv 5599	The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
|- ( `' `' A " B ) = ( A " B )
Theorem	dmsnn0 5600	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 } =/= (/) )