P. 51 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reseq2d 5001	Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C |` A ) = ( C |` B ) )
Theorem	reseq12d 5002	Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A |` C ) = ( B |` D ) )
Theorem	nfres 5003	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	csbresg 5004	Distribute proper substitution through the restriction of a class. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. V -> [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) )
Theorem	res0 5005	A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994.)
|- ( A |` (/) ) = (/)
Theorem	opelres 5006	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 5007	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 5008	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 5009	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 5010	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 5011	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 5012	<. 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 5013	The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)
|- ( ( A |` B ) |` C ) = ( A |` ( B i^i C ) )
Theorem	resundi 5014	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 5015	Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)
|- ( ( A u. B ) |` C ) = ( ( A |` C ) u. ( B |` C ) )
Theorem	resindi 5016	Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008.)
|- ( A |` ( B i^i C ) ) = ( ( A |` B ) i^i ( A |` C ) )
Theorem	resindir 5017	Class restriction distributes over intersection. (Contributed by NM, 18-Dec-2008.)
|- ( ( A i^i B ) |` C ) = ( ( A |` C ) i^i ( B |` C ) )
Theorem	inres 5018	Move intersection into class restriction. (Contributed by NM, 18-Dec-2008.)
|- ( A i^i ( B |` C ) ) = ( ( A i^i B ) |` C )
Theorem	resdifcom 5019	Commutative law for restriction and difference. (Contributed by AV, 7-Jun-2021.)
|- ( ( A |` B ) \ C ) = ( ( A \ C ) |` B )
Theorem	resiun1 5020*	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 5021*	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 5022	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 5023	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 5024	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 5025	A class includes its restriction. Exercise 15 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
|- ( A |` B ) C_ A
Theorem	rescom 5026	Commutative law for restriction. (Contributed by NM, 27-Mar-1998.)
|- ( ( A |` B ) |` C ) = ( ( A |` C ) |` B )
Theorem	ssres 5027	Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994.)
|- ( A C_ B -> ( A |` C ) C_ ( B |` C ) )
Theorem	ssres2 5028	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 5029	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 5030	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 5031	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 5032	Absorption law for restriction. (Contributed by NM, 27-Mar-1998.)
|- ( B C_ C -> ( ( A |` B ) |` C ) = ( A |` B ) )
Theorem	residm 5033	Idempotent law for restriction. (Contributed by NM, 27-Mar-1998.)
|- ( ( A |` B ) |` B ) = ( A |` B )
Theorem	resima 5034	A restriction to an image. (Contributed by NM, 29-Sep-2004.)
|- ( ( A |` B ) " B ) = ( A " B )
Theorem	resima2 5035	Image under a restricted class. (Contributed by FL, 31-Aug-2009.)
|- ( B C_ C -> ( ( A |` C ) " B ) = ( A " B ) )
Theorem	xpssres 5036	Restriction of a constant function (or other cross product). (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( C C_ A -> ( ( A X. B ) |` C ) = ( C X. B ) )
Theorem	elres 5037*	Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.)
|- ( A e. ( B |` C ) <-> E. x e. C E. y ( A = <. x , y >. /\ <. x , y >. e. B ) )
Theorem	elsnres 5038*	Memebership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011.)
|- C e. _V   =>    |- ( A e. ( B |` { C } ) <-> E. y ( A = <. C , y >. /\ <. C , y >. e. B ) )
Theorem	relssres 5039	Simplification law for restriction. (Contributed by NM, 16-Aug-1994.)
|- ( ( Rel A /\ dom A C_ B ) -> ( A |` B ) = A )
Theorem	resdm 5040	A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006.)
|- ( Rel A -> ( A |` dom A ) = A )
Theorem	resexg 5041	The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A e. V -> ( A |` B ) e. _V )
Theorem	resex 5042	The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.)
|- A e. _V   =>    |- ( A |` B ) e. _V
Theorem	resindm 5043	When restricting a relation, intersecting with the domain of the relation has no effect. (Contributed by FL, 6-Oct-2008.)
|- ( Rel A -> ( A |` ( B i^i dom A ) ) = ( A |` B ) )
Theorem	resdmdfsn 5044	Restricting a relation to its domain without a set is the same as restricting the relation to the universe without this set. (Contributed by AV, 2-Dec-2018.)
|- ( Rel R -> ( R |` ( _V \ { X } ) ) = ( R |` ( dom R \ { X } ) ) )
Theorem	resopab 5045*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002.)
|- ( { <. x , y >. | ph } |` A ) = { <. x , y >. | ( x e. A /\ ph ) }
Theorem	resiexg 5046	The existence of a restricted identity function, proved without using the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.)
|- ( A e. V -> ( _I |` A ) e. _V )
Theorem	iss 5047	A subclass of the identity function is the identity function restricted to its domain. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A C_ _I <-> A = ( _I |` dom A ) )
Theorem	resopab2 5048*	Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007.)
|- ( A C_ B -> ( { <. x , y >. | ( x e. B /\ ph ) } |` A ) = { <. x , y >. | ( x e. A /\ ph ) } )
Theorem	resmpt 5049*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)
|- ( B C_ A -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )
Theorem	resmpt3 5050*	Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro, 22-Mar-2015.)
|- ( ( x e. A |-> C ) |` B ) = ( x e. ( A i^i B ) |-> C )
Theorem	resmptf 5051	Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( B C_ A -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )
Theorem	resmptd 5052*	Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> B C_ A )   =>    |- ( ph -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )
Theorem	dfres2 5053*	Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- ( R |` A ) = { <. x , y >. | ( x e. A /\ x R y ) }
Theorem	opabresid 5054*	The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012.)
|- ( _I |` A ) = { <. x , y >. | ( x e. A /\ y = x ) }
Theorem	mptresid 5055*	The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.)
|- ( _I |` A ) = ( x e. A |-> x )
Theorem	dmresi 5056	The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.)
|- dom ( _I |` A ) = A
Theorem	restidsing 5057	Restriction of the identity to a singleton. (Contributed by FL, 2-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.) (Proof shortened by Peter Mazsa, 6-Oct-2022.)
|- ( _I |` { A } ) = ( { A } X. { A } )
Theorem	resid 5058	Any relation restricted to the universe is itself. (Contributed by NM, 16-Mar-2004.)
|- ( Rel A -> ( A |` _V ) = A )
Theorem	imaeq1 5059	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|- ( A = B -> ( A " C ) = ( B " C ) )
Theorem	imaeq2 5060	Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|- ( A = B -> ( C " A ) = ( C " B ) )
Theorem	imaeq1i 5061	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( A " C ) = ( B " C )
Theorem	imaeq2i 5062	Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|- A = B   =>    |- ( C " A ) = ( C " B )
Theorem	imaeq1d 5063	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A " C ) = ( B " C ) )
Theorem	imaeq2d 5064	Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C " A ) = ( C " B ) )
Theorem	imaeq12d 5065	Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A " C ) = ( B " D ) )
Theorem	dfima2 5066*	Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 19-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A " B ) = { y | E. x e. B x A y }
Theorem	dfima3 5067*	Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A " B ) = { y | E. x ( x e. B /\ <. x , y >. e. A ) }
Theorem	elimag 5068*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 20-Jan-2007.)
|- ( A e. V -> ( A e. ( B " C ) <-> E. x e. C x B A ) )
Theorem	elima 5069*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.)
|- A e. _V   =>    |- ( A e. ( B " C ) <-> E. x e. C x B A )
Theorem	elima2 5070*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.)
|- A e. _V   =>    |- ( A e. ( B " C ) <-> E. x ( x e. C /\ x B A ) )
Theorem	elima3 5071*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.)
|- A e. _V   =>    |- ( A e. ( B " C ) <-> E. x ( x e. C /\ <. x , A >. e. B ) )
Theorem	nfima 5072	Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A " B )
Theorem	nfimad 5073	Deduction version of bound-variable hypothesis builder nfima 5072. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x ( A " B ) )
Theorem	imadmrn 5074	The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.)
|- ( A " dom A ) = ran A
Theorem	imassrn 5075	The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.)
|- ( A " B ) C_ ran A
Theorem	mptima 5076*	Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ( x e. A |-> B ) " C ) = ran ( x e. ( A i^i C ) |-> B )
Theorem	mptimass 5077*	Image of a function in maps-to notation for a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> C C_ A )   =>    |- ( ph -> ( ( x e. A |-> B ) " C ) = ran ( x e. C |-> B ) )
Theorem	imaexg 5078	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.)
|- ( A e. V -> ( A " B ) e. _V )
Theorem	imaex 5079	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.)
|- A e. _V   =>    |- ( A " B ) e. _V
Theorem	imai 5080	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.)
|- ( _I " A ) = A
Theorem	rnresi 5081	The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.)
|- ran ( _I |` A ) = A
Theorem	resiima 5082	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
|- ( B C_ A -> ( ( _I |` A ) " B ) = B )
Theorem	ima0 5083	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)
|- ( A " (/) ) = (/)
Theorem	0ima 5084	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
|- ( (/) " A ) = (/)
Theorem	csbima12g 5085	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.)
|- ( A e. C -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )
Theorem	imadisj 5086	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 5087	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 5088	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 5089*	The image of a singleton. (Contributed by NM, 8-May-2005.)
|- ( A e. B -> ( R " { A } ) = { y | A R y } )
Theorem	elrelimasn 5090	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 5091	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 5092	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	args 5093*	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). (Contributed by NM, 8-May-2005.)
|- { x | E. y ( F " { x } ) = { y } } = { x | E! y x F y }
Theorem	eliniseg 5094	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 5095	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 5096*	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	dfse2 5097*	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	exse2 5098	Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- ( R e. V -> R Se A )
Theorem	imass1 5099	Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
|- ( A C_ B -> ( A " C ) C_ ( B " C ) )
Theorem	imass2 5100	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 ) )