P. 49 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4801-4900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opelco 4801*	Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. ( C o. D ) <-> E. x ( A D x /\ x C B ) )
Theorem	cnvss 4802	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> `' A C_ `' B )
Theorem	cnveq 4803	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|- ( A = B -> `' A = `' B )
Theorem	cnveqi 4804	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|- A = B   =>    |- `' A = `' B
Theorem	cnveqd 4805	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> `' A = `' B )
Theorem	elcnv 4806*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
|- ( A e. `' R <-> E. x E. y ( A = <. x , y >. /\ y R x ) )
Theorem	elcnv2 4807*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
|- ( A e. `' R <-> E. x E. y ( A = <. x , y >. /\ <. y , x >. e. R ) )
Theorem	nfcnv 4808	Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   =>    |- F/_ x `' A
Theorem	opelcnvg 4809	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 4810	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 4811	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 4812	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 4813	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 4814	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 4815*	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 4816*	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 4817*	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 4818*	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 4819*	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 4820*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( A e. V -> ( A e. ran B <-> E. x x B A ) )
Theorem	dfdm4 4821	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|- dom A = ran `' A
Theorem	dfdmf 4822*	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 4823	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 4824*	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 4825*	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 4826*	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 4827*	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 4828	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A C_ B -> dom A C_ dom B )
Theorem	dmeq 4829	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A = B -> dom A = dom B )
Theorem	dmeqi 4830	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- dom A = dom B
Theorem	dmeqd 4831	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> dom A = dom B )
Theorem	opeldm 4832	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 4833	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 4834	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 4835	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 4836	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 4837	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 4838	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 4839*	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 4840*	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 4841*	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 4842*	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 4843	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 4844	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 4845	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
|- dom _V = _V
Theorem	dm0rn0 4846	An empty domain implies an empty range. For a similar theorem for whether the domain and range are inhabited, see dmmrnm 4848. (Contributed by NM, 21-May-1998.)
|- ( dom A = (/) <-> ran A = (/) )
Theorem	reldm0 4847	A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> dom A = (/) ) )
Theorem	dmmrnm 4848*	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 4849*	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 4850	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 4851	The domain of the intersection of two square Cartesian products. Unlike dmin 4837, equality holds. (Contributed by NM, 29-Jan-2008.)
|- dom ( ( A X. A ) i^i ( B X. B ) ) = ( A i^i B )
Theorem	xpid11 4852	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 4853	The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5081). (Contributed by NM, 8-Apr-2007.)
|- dom `' `' A = dom A
Theorem	rncnvcnv 4854	The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
|- ran `' `' A = ran A
Theorem	elreldm 4855	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 4856	Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
|- ( A = B -> ran A = ran B )
Theorem	rneqi 4857	Equality inference for range. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- ran A = ran B
Theorem	rneqd 4858	Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> ran A = ran B )
Theorem	rnss 4859	Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> ran A C_ ran B )
Theorem	brelrng 4860	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 4861	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 4862	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 4863	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 4864	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 4865	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 4866*	Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. dom R <-> E. x A R x ) )
Theorem	relelrnb 4867*	Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. ran R <-> E. x x R A ) )
Theorem	releldmi 4868	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 4869	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 4870*	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 4871*	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 4872*	Membership in a range. (Contributed by NM, 2-Apr-2004.)
|- A e. _V   =>    |- ( A e. ran B <-> E. x x B A )
Theorem	nfdm 4873	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 4874	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 4875	Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
|- dom |^|_ x e. A B C_ |^|_ x e. A dom B
Theorem	rnopab 4876*	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 4877*	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 4878*	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 4879*	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 4880	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 4881*	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 4882*	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 4883*	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 4884*	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 4885	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 4886	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 4887	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 4888	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 4889	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 4890*	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 4891	A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> ran A = (/) ) )
Theorem	dmrnssfld 4892	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 4893	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 4894	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	dmex 4895	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 4896	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 4897	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 4898	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 4899	Range of a composition. (Contributed by NM, 19-Mar-1998.)
|- ran ( A o. B ) C_ ran A
Theorem	dmcosseq 4900	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 )