P. 50 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4901-5000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opelcnvg 4901	Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. `' R <-> <. B , A >. e. R ) )
Theorem	brcnvg 4902	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
|- ( ( A e. C /\ B e. D ) -> ( A `' R B <-> B R A ) )
Theorem	opelcnv 4903	Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. `' R <-> <. B , A >. e. R )
Theorem	brcnv 4904	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( A `' R B <-> B R A )
Theorem	csbcnvg 4905	Move class substitution in and out of the converse of a function. (Contributed by Thierry Arnoux, 8-Feb-2017.)
|- ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F )
Theorem	cnvco 4906	Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' ( A o. B ) = ( `' B o. `' A )
Theorem	cnvuni 4907*	The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
|- `' U. A = U_ x e. A `' x
Theorem	dfdm3 4908*	Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
|- dom A = { x | E. y <. x , y >. e. A }
Theorem	dfrn2 4909*	Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)
|- ran A = { y | E. x x A y }
Theorem	dfrn3 4910*	Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
|- ran A = { y | E. x <. x , y >. e. A }
Theorem	elrn2g 4911*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( A e. V -> ( A e. ran B <-> E. x <. x , A >. e. B ) )
Theorem	elrng 4912*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( A e. V -> ( A e. ran B <-> E. x x B A ) )
Theorem	ssrelrn 4913*	If a relation is a subset of a cartesian product, then for each element of the range of the relation there is an element of the first set of the cartesian product which is related to the element of the range by the relation. (Contributed by AV, 24-Oct-2020.)
|- ( ( R C_ ( A X. B ) /\ Y e. ran R ) -> E. a e. A a R Y )
Theorem	dfdm4 4914	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|- dom A = ran `' A
Theorem	dfdmf 4915*	Definition of domain, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   &    |- F/_ y A   =>    |- dom A = { x | E. y x A y }
Theorem	csbdmg 4916	Distribute proper substitution through the domain of a class. (Contributed by Jim Kingdon, 8-Dec-2018.)
|- ( A e. V -> [_ A / x ]_ dom B = dom [_ A / x ]_ B )
Theorem	eldmg 4917*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> ( A e. dom B <-> E. y A B y ) )
Theorem	eldm2g 4918*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> ( A e. dom B <-> E. y <. A , y >. e. B ) )
Theorem	eldm 4919*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
|- A e. _V   =>    |- ( A e. dom B <-> E. y A B y )
Theorem	eldm2 4920*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)
|- A e. _V   =>    |- ( A e. dom B <-> E. y <. A , y >. e. B )
Theorem	dmss 4921	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A C_ B -> dom A C_ dom B )
Theorem	dmeq 4922	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A = B -> dom A = dom B )
Theorem	dmeqi 4923	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- dom A = dom B
Theorem	dmeqd 4924	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> dom A = dom B )
Theorem	opeldm 4925	Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. C -> A e. dom C )
Theorem	breldm 4926	Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( A R B -> A e. dom R )
Theorem	opeldmg 4927	Membership of first of an ordered pair in a domain. (Contributed by Jim Kingdon, 9-Jul-2019.)
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. C -> A e. dom C ) )
Theorem	breldmg 4928	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 4929	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 4930	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 4931	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 4932*	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 4933*	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 4934*	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 4935*	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 4936	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 4937	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 4938	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
|- dom _V = _V
Theorem	dm0rn0 4939	An empty domain implies an empty range. For a similar theorem for whether the domain and range are inhabited, see dmmrnm 4942. (Contributed by NM, 21-May-1998.)
|- ( dom A = (/) <-> ran A = (/) )
Theorem	reldm0 4940	A relation is empty iff its domain is empty. For a similar theorem for whether the relation and domain are inhabited, see reldmm 4941. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> dom A = (/) ) )
Theorem	reldmm 4941*	A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.)
|- ( Rel A -> ( E. x x e. A <-> E. y y e. dom A ) )
Theorem	dmmrnm 4942*	A domain is inhabited if and only if the range is inhabited. (Contributed by Jim Kingdon, 15-Dec-2018.)
|- ( E. x x e. dom A <-> E. y y e. ran A )
Theorem	dmxpm 4943*	The domain of a cross 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.)
|- ( E. x x e. B -> dom ( A X. B ) = A )
Theorem	dmxpid 4944	The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.) (Revised by Jim Kingdon, 11-Apr-2023.)
|- dom ( A X. A ) = A
Theorem	dmxpin 4945	The domain of the intersection of two square Cartesian products. Unlike dmin 4930, equality holds. (Contributed by NM, 29-Jan-2008.)
|- dom ( ( A X. A ) i^i ( B X. B ) ) = ( A i^i B )
Theorem	xpid11 4946	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 4947	The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5178). (Contributed by NM, 8-Apr-2007.)
|- dom `' `' A = dom A
Theorem	rncnvcnv 4948	The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
|- ran `' `' A = ran A
Theorem	elreldm 4949	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 4950	Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
|- ( A = B -> ran A = ran B )
Theorem	rneqi 4951	Equality inference for range. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- ran A = ran B
Theorem	rneqd 4952	Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> ran A = ran B )
Theorem	rnss 4953	Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> ran A C_ ran B )
Theorem	brelrng 4954	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	opelrng 4955	Membership of second member of an ordered pair in a range. (Contributed by Jim Kingdon, 26-Jan-2019.)
|- ( ( A e. F /\ B e. G /\ <. A , B >. e. C ) -> B e. ran C )
Theorem	brelrn 4956	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 4957	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 4958	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 4959	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 4960*	Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. dom R <-> E. x A R x ) )
Theorem	relelrnb 4961*	Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. ran R <-> E. x x R A ) )
Theorem	releldmi 4962	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 4963	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 4964*	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 4965*	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 4966*	Membership in a range. (Contributed by NM, 2-Apr-2004.)
|- A e. _V   =>    |- ( A e. ran B <-> E. x x B A )
Theorem	nfdm 4967	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 4968	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 4969	Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
|- dom |^|_ x e. A B C_ |^|_ x e. A dom B
Theorem	rnopab 4970*	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 4971*	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 4972*	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 4973*	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 4974	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 4975*	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 4976*	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	elrnmptdv 4977*	Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- F = ( x e. A |-> B )   &    |- ( ph -> C e. A )   &    |- ( ph -> D e. V )   &    |- ( ( ph /\ x = C ) -> D = B )   =>    |- ( ph -> D e. ran F )
Theorem	elrnmpt2d 4978*	Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- F = ( x e. A |-> B )   &    |- ( ph -> C e. ran F )   =>    |- ( ph -> E. x e. A C = B )
Theorem	rn0 4979	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 4980	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 4981	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 4982	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 4983	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 4984*	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 4985	A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> ran A = (/) ) )
Theorem	dmrnssfld 4986	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	dmexg 4987	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.)
|- ( A e. V -> dom A e. _V )
Theorem	rnexg 4988	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.)
|- ( A e. V -> ran A e. _V )
Theorem	dmexd 4989	The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   =>    |- ( ph -> dom A e. _V )
Theorem	dmex 4990	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.)
|- A e. _V   =>    |- dom A e. _V
Theorem	rnex 4991	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 7-Jul-2008.)
|- A e. _V   =>    |- ran A e. _V
Theorem	iprc 4992	The identity function is a proper class. This means, for example, that we cannot use it as a member of the class of continuous functions unless it is restricted to a set. (Contributed by NM, 1-Jan-2007.)
|- -. _I e. _V
Theorem	dmcoss 4993	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 4994	Range of a composition. (Contributed by NM, 19-Mar-1998.)
|- ran ( A o. B ) C_ ran A
Theorem	dmcosseq 4995	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 4996	Domain of a composition. (Contributed by NM, 19-Mar-1998.)
|- ( dom A = ran B -> dom ( A o. B ) = dom B )
Theorem	rncoeq 4997	Range of a composition. (Contributed by NM, 19-Mar-1998.)
|- ( dom A = ran B -> ran ( A o. B ) = ran A )
Theorem	reseq1 4998	Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.)
|- ( A = B -> ( A |` C ) = ( B |` C ) )
Theorem	reseq2 4999	Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)
|- ( A = B -> ( C |` A ) = ( C |` B ) )
Theorem	reseq1i 5000	Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
|- A = B   =>    |- ( A |` C ) = ( B |` C )