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	raliunxp 4901*	Write a double restricted quantification as one universal quantifier. In this version of ralxp 4903, B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( A. x e. U_ y e. A ( { y } X. B ) ph <-> A. y e. A A. z e. B ps )
Theorem	rexiunxp 4902*	Write a double restricted quantification as one universal quantifier. In this version of rexxp 4904, B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( E. x e. U_ y e. A ( { y } X. B ) ph <-> E. y e. A E. z e. B ps )
Theorem	ralxp 4903*	Universal quantification restricted to a cross product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )
Theorem	rexxp 4904*	Existential quantification restricted to a cross product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
|- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )
Theorem	djussxp 4905*	Disjoint union is a subset of a cross product. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|- U_ x e. A ( { x } X. B ) C_ ( A X. _V )
Theorem	ralxpf 4906*	Version of ralxp 4903 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- F/ z ph   &    |- F/ x ps   &    |- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )
Theorem	rexxpf 4907*	Version of rexxp 4904 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- F/ z ph   &    |- F/ x ps   &    |- ( x = <. y , z >. -> ( ph <-> ps ) )   =>    |- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )
Theorem	iunxpf 4908*	Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
|- F/_ y C   &    |- F/_ z C   &    |- F/_ x D   &    |- ( x = <. y , z >. -> C = D )   =>    |- U_ x e. ( A X. B ) C = U_ y e. A U_ z e. B D
Theorem	opabbi2dv 4909*	Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2355. (Contributed by NM, 24-Feb-2014.)
|- Rel A   &    |- ( ph -> ( <. x , y >. e. A <-> ps ) )   =>    |- ( ph -> A = { <. x , y >. | ps } )
Theorem	relop 4910*	A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)
|- A e. _V   &    |- B e. _V   =>    |- ( Rel <. A , B >. <-> E. x E. y ( A = { x } /\ B = { x , y } ) )
Theorem	ideqg 4911	For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( B e. V -> ( A _I B <-> A = B ) )
Theorem	ideq 4912	For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)
|- B e. _V   =>    |- ( A _I B <-> A = B )
Theorem	ididg 4913	A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( A e. V -> A _I A )
Theorem	issetid 4914	Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A e. _V <-> A _I A )
Theorem	coss1 4915	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|- ( A C_ B -> ( A o. C ) C_ ( B o. C ) )
Theorem	coss2 4916	Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|- ( A C_ B -> ( C o. A ) C_ ( C o. B ) )
Theorem	coeq1 4917	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- ( A = B -> ( A o. C ) = ( B o. C ) )
Theorem	coeq2 4918	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- ( A = B -> ( C o. A ) = ( C o. B ) )
Theorem	coeq1i 4919	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>    |- ( A o. C ) = ( B o. C )
Theorem	coeq2i 4920	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>    |- ( C o. A ) = ( C o. B )
Theorem	coeq1d 4921	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A o. C ) = ( B o. C ) )
Theorem	coeq2d 4922	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C o. A ) = ( C o. B ) )
Theorem	coeq12i 4923	Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
|- A = B   &    |- C = D   =>    |- ( A o. C ) = ( B o. D )
Theorem	coeq12d 4924	Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A o. C ) = ( B o. D ) )
Theorem	nfco 4925	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A o. B )
Theorem	elco 4926*	Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
|- ( A e. ( R o. S ) <-> E. x E. y E. z ( A = <. x , z >. /\ ( x S y /\ y R z ) ) )
Theorem	brcog 4927*	Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)
|- ( ( A e. V /\ B e. W ) -> ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) ) )
Theorem	opelco2g 4928*	Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. ( C o. D ) <-> E. x ( <. A , x >. e. D /\ <. x , B >. e. C ) ) )
Theorem	brcogw 4929	Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.)
|- ( ( ( A e. V /\ B e. W /\ X e. Z ) /\ ( A D X /\ X C B ) ) -> A ( C o. D ) B )
Theorem	eqbrrdva 4930*	Deduction from extensionality principle for relations, given an equivalence only on the relation's domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.)
|- ( ph -> A C_ ( C X. D ) )   &    |- ( ph -> B C_ ( C X. D ) )   &    |- ( ( ph /\ x e. C /\ y e. D ) -> ( x A y <-> x B y ) )   =>    |- ( ph -> A = B )
Theorem	brco 4931*	Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ( C o. D ) B <-> E. x ( A D x /\ x C B ) )
Theorem	opelco 4932*	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 4933	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> `' A C_ `' B )
Theorem	cnveq 4934	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|- ( A = B -> `' A = `' B )
Theorem	cnveqi 4935	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|- A = B   =>    |- `' A = `' B
Theorem	cnveqd 4936	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> `' A = `' B )
Theorem	elcnv 4937*	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 4938*	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 4939	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 4940	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 4941	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 4942	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 4943	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 4944	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 4945	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 4946*	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 4947*	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 4948*	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 4949*	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 4950*	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 4951*	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 4952*	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 4953	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|- dom A = ran `' A
Theorem	dfdmf 4954*	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 4955	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 4956*	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 4957*	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 4958*	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 4959*	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 4960	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A C_ B -> dom A C_ dom B )
Theorem	dmeq 4961	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- ( A = B -> dom A = dom B )
Theorem	dmeqi 4962	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- dom A = dom B
Theorem	dmeqd 4963	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> dom A = dom B )
Theorem	opeldm 4964	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 4965	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 4966	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 4967	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 4968	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 4969	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 4970	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 4971*	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 4972*	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 4973*	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 4974*	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 4975	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 4976	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 4977	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
|- dom _V = _V
Theorem	dm0rn0 4978	An empty domain implies an empty range. For a similar theorem for whether the domain and range are inhabited, see dmmrnm 4981. (Contributed by NM, 21-May-1998.)
|- ( dom A = (/) <-> ran A = (/) )
Theorem	reldm0 4979	A relation is empty iff its domain is empty. For a similar theorem for whether the relation and domain are inhabited, see reldmm 4980. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> ( A = (/) <-> dom A = (/) ) )
Theorem	reldmm 4980*	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 4981*	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 4982*	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 4983	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 4984	The domain of the intersection of two square Cartesian products. Unlike dmin 4969, equality holds. (Contributed by NM, 29-Jan-2008.)
|- dom ( ( A X. A ) i^i ( B X. B ) ) = ( A i^i B )
Theorem	xpid11 4985	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 4986	The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5218). (Contributed by NM, 8-Apr-2007.)
|- dom `' `' A = dom A
Theorem	rncnvcnv 4987	The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
|- ran `' `' A = ran A
Theorem	elreldm 4988	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 4989	Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
|- ( A = B -> ran A = ran B )
Theorem	rneqi 4990	Equality inference for range. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>    |- ran A = ran B
Theorem	rneqd 4991	Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> ran A = ran B )
Theorem	rnss 4992	Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
|- ( A C_ B -> ran A C_ ran B )
Theorem	brelrng 4993	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 4994	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 4995	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 4996	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 4997	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 4998	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 4999*	Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. dom R <-> E. x A R x ) )
Theorem	relelrnb 5000*	Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
|- ( Rel R -> ( A e. ran R <-> E. x x R A ) )