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	breldmg 5201	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 5202	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 5203	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 5204	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 5205*	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 5206*	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 5207*	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 5208*	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 5209	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 5210	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 5211	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
|- dom _V = _V
Theorem	dm0rn0 5212	An empty domain implies an empty range. (Contributed by NM, 21-May-1998.)
|- ( dom A = (/) <-> ran A = (/) )
Theorem	reldm0 5213	A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> dom A = (/) ) )
Theorem	dmxp 5214	The domain of a Cartesian 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.)
|- ( B =/= (/) -> dom ( A X. B ) = A )
Theorem	dmxpid 5215	The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.)
|- dom ( A X. A ) = A
Theorem	dmxpin 5216	The domain of the intersection of two square Cartesian products. Unlike dmin 5203, equality holds. (Contributed by NM, 29-Jan-2008.)
|- dom ( ( A X. A ) i^i ( B X. B ) ) = ( A i^i B )
Theorem	xpid11 5217	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 )
Theorem	dmcnvcnv 5218	The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5450). (Contributed by NM, 8-Apr-2007.)
|- dom `' `' A = dom A
Theorem	rncnvcnv 5219	The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
|- ran `' `' A = ran A
Theorem	elreldm 5220	The first member of an ordered pair in a relation belongs to the domain of the relation. (Contributed by NM, 28-Jul-2004.)
|- ( ( Rel A /\ B e. A ) -> |^| |^| B e. dom A )
Theorem	rneq 5221	Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
|- ( A = B -> ran A = ran B )
Theorem	rneqi 5222	Equality inference for range. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- ran A = ran B
Theorem	rneqd 5223	Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> ran A = ran B )
Theorem	rnss 5224	Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> ran A C_ ran B )
Theorem	brelrng 5225	The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.)
|- ( ( A e. F /\ B e. G /\ A C B ) -> B e. ran C )
Theorem	brelrn 5226	The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.)
|- A e. _V   &    |- B e. _V   =>    |- ( A C B -> B e. ran C )
Theorem	opelrn 5227	Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. C -> B e. ran C )
Theorem	releldm 5228	The first argument of a binary relation belongs to its domain. (Contributed by NM, 2-Jul-2008.)
|- ( ( Rel R /\ A R B ) -> A e. dom R )
Theorem	relelrn 5229	The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.)
|- ( ( Rel R /\ A R B ) -> B e. ran R )
Theorem	releldmb 5230*	Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. dom R <-> E. x A R x ) )
Theorem	relelrnb 5231*	Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. ran R <-> E. x x R A ) )
Theorem	releldmi 5232	The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.)
|- Rel R   =>    |- ( A R B -> A e. dom R )
Theorem	relelrni 5233	The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.)
|- Rel R   =>    |- ( A R B -> B e. ran R )
Theorem	dfrnf 5234*	Definition of range, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   &    |- F/_ y A   =>    |- ran A = { y | E. x x A y }
Theorem	elrn2 5235*	Membership in a range. (Contributed by NM, 10-Jul-1994.)
|- A e. _V   =>    |- ( A e. ran B <-> E. x <. x , A >. e. B )
Theorem	elrn 5236*	Membership in a range. (Contributed by NM, 2-Apr-2004.)
|- A e. _V   =>    |- ( A e. ran B <-> E. x x B A )
Theorem	nfdm 5237	Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   =>    |- F/_ x dom A
Theorem	nfrn 5238	Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   =>    |- F/_ x ran A
Theorem	dmiin 5239	Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
|- dom |^|_ x e. A B C_ |^|_ x e. A dom B
Theorem	rnopab 5240*	The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|- ran { <. x , y >. | ph } = { y | E. x ph }
Theorem	rnmpt 5241*	The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- F = ( x e. A |-> B )   =>    |- ran F = { y | E. x e. A y = B }
Theorem	elrnmpt 5242*	The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.)
|- F = ( x e. A |-> B )   =>    |- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )
Theorem	elrnmpt1s 5243*	Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.)
|- F = ( x e. A |-> B )   &    |- ( x = D -> B = C )   =>    |- ( ( D e. A /\ C e. V ) -> C e. ran F )
Theorem	elrnmpt1 5244	Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- F = ( x e. A |-> B )   =>    |- ( ( x e. A /\ B e. V ) -> B e. ran F )
Theorem	elrnmptg 5245*	Membership in the range of a function. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- F = ( x e. A |-> B )   =>    |- ( A. x e. A B e. V -> ( C e. ran F <-> E. x e. A C = B ) )
Theorem	elrnmpti 5246*	Membership in the range of a function. (Contributed by NM, 30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- F = ( x e. A |-> B )   &    |- B e. _V   =>    |- ( C e. ran F <-> E. x e. A C = B )
Theorem	rn0 5247	The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.)
|- ran (/) = (/)
Theorem	dfiun3g 5248	Alternate definition of indexed union when B is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( A. x e. A B e. C -> U_ x e. A B = U. ran ( x e. A |-> B ) )
Theorem	dfiin3g 5249	Alternate definition of indexed intersection when B is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( A. x e. A B e. C -> |^|_ x e. A B = |^| ran ( x e. A |-> B ) )
Theorem	dfiun3 5250	Alternate definition of indexed union when B is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- B e. _V   =>    |- U_ x e. A B = U. ran ( x e. A |-> B )
Theorem	dfiin3 5251	Alternate definition of indexed intersection when B is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- B e. _V   =>    |- |^|_ x e. A B = |^| ran ( x e. A |-> B )
Theorem	riinint 5252*	Express a relative indexed intersection as an intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( X e. V /\ A. k e. I S C_ X ) -> ( X i^i |^|_ k e. I S ) = |^| ( { X } u. ran ( k e. I |-> S ) ) )
Theorem	relrn0 5253	A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> ran A = (/) ) )
Theorem	dmrnssfld 5254	The domain and range of a class are included in its double union. (Contributed by NM, 13-May-2008.)
|- ( dom A u. ran A ) C_ U. U. A
Theorem	dmcoss 5255	Domain of a composition. Theorem 21 of [Suppes] p. 63. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- dom ( A o. B ) C_ dom B
Theorem	rncoss 5256	Range of a composition. (Contributed by NM, 19-Mar-1998.)
|- ran ( A o. B ) C_ ran A
Theorem	dmcosseq 5257	Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ran B C_ dom A -> dom ( A o. B ) = dom B )
Theorem	dmcoeq 5258	Domain of a composition. (Contributed by NM, 19-Mar-1998.)
|- ( dom A = ran B -> dom ( A o. B ) = dom B )
Theorem	rncoeq 5259	Range of a composition. (Contributed by NM, 19-Mar-1998.)
|- ( dom A = ran B -> ran ( A o. B ) = ran A )
Theorem	reseq1 5260	Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.)
|- ( A = B -> ( A |` C ) = ( B |` C ) )
Theorem	reseq2 5261	Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)
|- ( A = B -> ( C |` A ) = ( C |` B ) )
Theorem	reseq1i 5262	Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
|- A = B   =>    |- ( A |` C ) = ( B |` C )
Theorem	reseq2i 5263	Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- A = B   =>    |- ( C |` A ) = ( C |` B )
Theorem	reseq12i 5264	Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
|- A = B   &    |- C = D   =>    |- ( A |` C ) = ( B |` D )
Theorem	reseq1d 5265	Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A |` C ) = ( B |` C ) )
Theorem	reseq2d 5266	Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C |` A ) = ( C |` B ) )
Theorem	reseq12d 5267	Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A |` C ) = ( B |` D ) )
Theorem	nfres 5268	Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A |` B )
Theorem	csbres 5269	Distribute proper substitution through the restriction of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 23-Aug-2018.)
|- [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C )
Theorem	csbresgOLD 5270	Distribute proper substitution through the restriction of a class. csbresgOLD 5270 is derived from the virtual deduction proof csbresgVD 32652. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbres 5269 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) )
Theorem	res0 5271	A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994.)
|- ( A |` (/) ) = (/)
Theorem	opelres 5272	Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.)
|- B e. _V   =>    |- ( <. A , B >. e. ( C |` D ) <-> ( <. A , B >. e. C /\ A e. D ) )
Theorem	brres 5273	Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.)
|- B e. _V   =>    |- ( A ( C |` D ) B <-> ( A C B /\ A e. D ) )
Theorem	opelresg 5274	Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 14-Oct-2005.)
|- ( B e. V -> ( <. A , B >. e. ( C |` D ) <-> ( <. A , B >. e. C /\ A e. D ) ) )
Theorem	brresg 5275	Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.)
|- ( B e. V -> ( A ( C |` D ) B <-> ( A C B /\ A e. D ) ) )
Theorem	opres 5276	Ordered pair membership in a restriction when the first member belongs to the restricting class. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- B e. _V   =>    |- ( A e. D -> ( <. A , B >. e. ( C |` D ) <-> <. A , B >. e. C ) )
Theorem	resieq 5277	A restricted identity relation is equivalent to equality in its domain. (Contributed by NM, 30-Apr-2004.)
|- ( ( B e. A /\ C e. A ) -> ( B ( _I |` A ) C <-> B = C ) )
Theorem	opelresi 5278	<. A , A >. belongs to a restriction of the identity class iff A belongs to the restricting class. (Contributed by FL, 27-Oct-2008.) (Revised by NM, 30-Mar-2016.)
|- ( A e. V -> ( <. A , A >. e. ( _I |` B ) <-> A e. B ) )
Theorem	resres 5279	The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)
|- ( ( A |` B ) |` C ) = ( A |` ( B i^i C ) )
Theorem	resundi 5280	Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
|- ( A |` ( B u. C ) ) = ( ( A |` B ) u. ( A |` C ) )
Theorem	resundir 5281	Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)
|- ( ( A u. B ) |` C ) = ( ( A |` C ) u. ( B |` C ) )
Theorem	resindi 5282	Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.)
|- ( A |` ( B i^i C ) ) = ( ( A |` B ) i^i ( A |` C ) )
Theorem	resindir 5283	Class restriction distributes over intersection. (Contributed by NM, 18-Dec-2008.)
|- ( ( A i^i B ) |` C ) = ( ( A |` C ) i^i ( B |` C ) )
Theorem	inres 5284	Move intersection into class restriction. (Contributed by NM, 18-Dec-2008.)
|- ( A i^i ( B |` C ) ) = ( ( A i^i B ) |` C )
Theorem	resiun1 5285*	Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
|- ( U_ x e. A B |` C ) = U_ x e. A ( B |` C )
Theorem	resiun2 5286*	Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
|- ( C |` U_ x e. A B ) = U_ x e. A ( C |` B )
Theorem	dmres 5287	The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.)
|- dom ( A |` B ) = ( B i^i dom A )
Theorem	ssdmres 5288	A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.)
|- ( A C_ dom B <-> dom ( B |` A ) = A )
Theorem	dmresexg 5289	The domain of a restriction to a set exists. (Contributed by NM, 7-Apr-1995.)
|- ( B e. V -> dom ( A |` B ) e. _V )
Theorem	resss 5290	A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
|- ( A |` B ) C_ A
Theorem	rescom 5291	Commutative law for restriction. (Contributed by NM, 27-Mar-1998.)
|- ( ( A |` B ) |` C ) = ( ( A |` C ) |` B )
Theorem	ssres 5292	Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.)
|- ( A C_ B -> ( A |` C ) C_ ( B |` C ) )
Theorem	ssres2 5293	Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A C_ B -> ( C |` A ) C_ ( C |` B ) )
Theorem	relres 5294	A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- Rel ( A |` B )
Theorem	resabs1 5295	Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.)
|- ( B C_ C -> ( ( A |` C ) |` B ) = ( A |` B ) )
Theorem	resabs1d 5296	Absorption law for restriction, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> B C_ C )   =>    |- ( ph -> ( ( A |` C ) |` B ) = ( A |` B ) )
Theorem	resabs2 5297	Absorption law for restriction. (Contributed by NM, 27-Mar-1998.)
|- ( B C_ C -> ( ( A |` B ) |` C ) = ( A |` B ) )
Theorem	residm 5298	Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.)
|- ( ( A |` B ) |` B ) = ( A |` B )
Theorem	resima 5299	A restriction to an image. (Contributed by NM, 29-Sep-2004.)
|- ( ( A |` B ) " B ) = ( A " B )
Theorem	resima2 5300	Image under a restricted class. (Contributed by FL, 31-Aug-2009.)
|- ( B C_ C -> ( ( A |` C ) " B ) = ( A " B ) )