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	cnvss 4901	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> `' A C_ `' B )
Theorem	cnveq 4902	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|- ( A = B -> `' A = `' B )
Theorem	cnveqi 4903	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|- A = B   =>    |- `' A = `' B
Theorem	cnveqd 4904	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> `' A = `' B )
Theorem	elcnv 4905*	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 4906*	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 4907	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 4908	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 4909	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 4910	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 4911	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 4912	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 4913	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 4914*	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 4915*	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 4916*	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 4917*	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 4918*	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 4919*	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 4920*	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 4921	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|- dom A = ran `' A
Theorem	dfdmf 4922*	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 4923	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 4924*	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 4925*	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 4926*	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 4927*	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 4928	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A C_ B -> dom A C_ dom B )
Theorem	dmeq 4929	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A = B -> dom A = dom B )
Theorem	dmeqi 4930	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- dom A = dom B
Theorem	dmeqd 4931	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> dom A = dom B )
Theorem	opeldm 4932	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 4933	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 4934	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 4935	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 4936	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 4937	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 4938	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 4939*	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 4940*	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 4941*	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 4942*	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 4943	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 4944	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 4945	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
|- dom _V = _V
Theorem	dm0rn0 4946	An empty domain implies an empty range. For a similar theorem for whether the domain and range are inhabited, see dmmrnm 4949. (Contributed by NM, 21-May-1998.)
|- ( dom A = (/) <-> ran A = (/) )
Theorem	reldm0 4947	A relation is empty iff its domain is empty. For a similar theorem for whether the relation and domain are inhabited, see reldmm 4948. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> dom A = (/) ) )
Theorem	reldmm 4948*	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 4949*	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 4950*	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 4951	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 4952	The domain of the intersection of two square Cartesian products. Unlike dmin 4937, equality holds. (Contributed by NM, 29-Jan-2008.)
|- dom ( ( A X. A ) i^i ( B X. B ) ) = ( A i^i B )
Theorem	xpid11 4953	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 4954	The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5185). (Contributed by NM, 8-Apr-2007.)
|- dom `' `' A = dom A
Theorem	rncnvcnv 4955	The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
|- ran `' `' A = ran A
Theorem	elreldm 4956	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 4957	Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
|- ( A = B -> ran A = ran B )
Theorem	rneqi 4958	Equality inference for range. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- ran A = ran B
Theorem	rneqd 4959	Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> ran A = ran B )
Theorem	rnss 4960	Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> ran A C_ ran B )
Theorem	brelrng 4961	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 4962	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 4963	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 4964	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 4965	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 4966	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 4967*	Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. dom R <-> E. x A R x ) )
Theorem	relelrnb 4968*	Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. ran R <-> E. x x R A ) )
Theorem	releldmi 4969	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 4970	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 4971*	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 4972*	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 4973*	Membership in a range. (Contributed by NM, 2-Apr-2004.)
|- A e. _V   =>    |- ( A e. ran B <-> E. x x B A )
Theorem	nfdm 4974	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 4975	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 4976	Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
|- dom |^|_ x e. A B C_ |^|_ x e. A dom B
Theorem	rnopab 4977*	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 4978*	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 4979*	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 4980*	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 4981	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 4982*	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 4983*	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 4984*	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 4985*	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 4986	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 4987	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 4988	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 4989	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 4990	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 4991*	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 4992	A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> ran A = (/) ) )
Theorem	dmrnssfld 4993	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 4994	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 4995	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 4996	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 4997	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 4998	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 4999	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 5000	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