P. 45 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4401-4500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reliun 4401	An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.)
|- ( Rel U_x e. A B <-> A.x e. A Rel B)
Theorem	reliin 4402	An indexed intersection is a relation if at least one of the member of the indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
|- (E.x e. A Rel B -> Rel |^|_x e. A B)
Theorem	reluni 4403*	The union of a class is a relation iff any member is a relation. Exercise 6 of [TakeutiZaring] p. 25 and its converse. (Contributed by NM, 13-Aug-2004.)
|- ( Rel U.A <-> A.x e. A Rel x)
Theorem	relint 4404*	The intersection of a class is a relation if at least one member is a relation. (Contributed by NM, 8-Mar-2014.)
|- (E.x e. A Rel x -> Rel |^|A)
Theorem	rel0 4405	The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
|- Rel (/)
Theorem	relopabi 4406	A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.)
|- A = { <.x , y >. | ph }   =>   |- Rel A
Theorem	relopab 4407	A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) (Unnecessary distinct variable restrictions were removed by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
|- Rel { <.x , y >. | ph }
Theorem	reli 4408	The identity relation is a relation. Part of Exercise 4.12(p) of [Mendelson] p. 235. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- Rel _I
Theorem	rele 4409	The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- Rel _E
Theorem	opabid2 4410*	A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006.)
|- ( Rel A -> { <.x , y >. | <.x , y >. e. A } = A)
Theorem	inopab 4411*	Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ( { <.x , y >. | ph } i^i { <.x , y >. | ps }) = { <.x , y >. | (ph /\ ps) }
Theorem	difopab 4412*	The difference of two ordered-pair abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( { <.x , y >. | ph } \ { <.x , y >. | ps }) = { <.x , y >. | (ph /\ -. ps) }
Theorem	inxp 4413	The intersection of two cross products. Exercise 9 of [TakeutiZaring] p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ((A X. B) i^i ( C X. D)) = ((A i^i C) X. (B i^i D))
Theorem	xpindi 4414	Distributive law for cross product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
|- (A X. (B i^i C)) = ((A X. B) i^i (A X. C))
Theorem	xpindir 4415	Distributive law for cross product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
|- ((A i^i B) X. C) = ((A X. C) i^i (B X. C))
Theorem	xpiindim 4416*	Distributive law for cross product over indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|- (E.y y e. A -> ( C X. |^|_x e. A B) = |^|_x e. A ( C X. B))
Theorem	xpriindim 4417*	Distributive law for cross product over relativized indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|- (E.y y e. A -> ( C X. ( D i^i |^|_x e. A B)) = (( C X. D) i^i |^|_x e. A ( C X. B)))
Theorem	eliunxp 4418*	Membership in a union of cross products. Analogue of elxp 4305 for nonconstant B(x). (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( C e. U_x e. A ( {x } X. B) <-> E.xE.y( C = <.x , y >. /\ (x e. A /\ y e. B)))
Theorem	opeliunxp2 4419*	Membership in a union of cross products. (Contributed by Mario Carneiro, 14-Feb-2015.)
|- (x = C -> B = E)   =>   |- ( <. C , D >. e. U_x e. A ( {x } X. B) <-> ( C e. A /\ D e. E))
Theorem	raliunxp 4420*	Write a double restricted quantification as one universal quantifier. In this version of ralxp 4422, 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 4421*	Write a double restricted quantification as one universal quantifier. In this version of rexxp 4423, 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 4422*	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 4423*	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 4424*	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 4425*	Version of ralxp 4422 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/yph   &   |- F/zph   &   |- F/xps   &   |- (x = <.y , z >. -> (ph <-> ps))   =>   |- (A.x e. (A X. B)ph <-> A.y e. A A.z e. B ps)
Theorem	rexxpf 4426*	Version of rexxp 4423 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/yph   &   |- F/zph   &   |- F/xps   &   |- (x = <.y , z >. -> (ph <-> ps))   =>   |- (E.x e. (A X. B)ph <-> E.y e. A E.z e. B ps)
Theorem	iunxpf 4427*	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 4428*	Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2153. (Contributed by NM, 24-Feb-2014.)
|- Rel A   &   |- (ph -> ( <.x , y >. e. A <-> ps))   =>   |- (ph -> A = { <.x , y >. | ps })
Theorem	relop 4429*	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.xE.y(A = {x } /\ B = {x , y }))
Theorem	ideqg 4430	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 4431	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 4432	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 4433	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 4434	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|- (A C_ B -> (A o. C) C_ (B o. C))
Theorem	coss2 4435	Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|- (A C_ B -> ( C o. A) C_ ( C o. B))
Theorem	coeq1 4436	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- (A = B -> (A o. C) = (B o. C))
Theorem	coeq2 4437	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
|- (A = B -> ( C o. A) = ( C o. B))
Theorem	coeq1i 4438	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>   |- (A o. C) = (B o. C)
Theorem	coeq2i 4439	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
|- A = B   =>   |- ( C o. A) = ( C o. B)
Theorem	coeq1d 4440	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 4441	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 4442	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 4443	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 4444	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(A o. B)
Theorem	brcog 4445*	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 Dx /\ x CB)))
Theorem	opelco2g 4446*	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 4447	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 CB)) -> A( C o. D)B)
Theorem	eqbrrdva 4448*	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) -> (xAy <-> xBy))   =>   |- (ph -> A = B)
Theorem	brco 4449*	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 Dx /\ x CB))
Theorem	opelco 4450*	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 Dx /\ x CB))
Theorem	cnvss 4451	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|- (A C_ B -> `'A C_ `'B)
Theorem	cnveq 4452	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|- (A = B -> `'A = `'B)
Theorem	cnveqi 4453	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|- A = B   =>   |- `'A = `'B
Theorem	cnveqd 4454	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|- (ph -> A = B)   =>   |- (ph -> `'A = `'B)
Theorem	elcnv 4455*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
|- (A e. `' R <-> E.xE.y(A = <.x , y >. /\ y Rx))
Theorem	elcnv2 4456*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
|- (A e. `' R <-> E.xE.y(A = <.x , y >. /\ <.y , x >. e. R))
Theorem	nfcnv 4457	Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_xA   =>   |- F/_x `'A
Theorem	opelcnvg 4458	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 4459	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 `' RB <-> B RA))
Theorem	opelcnv 4460	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 4461	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 `' RB <-> B RA)
Theorem	csbcnvg 4462	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 4463	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 4464*	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 4465*	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 4466*	Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)
|- ran A = {y | E.x xAy }
Theorem	dfrn3 4467*	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 4468*	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 4469*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|- (A e. V -> (A e. ran B <-> E.x xBA))
Theorem	dfdm4 4470	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|- dom A = ran `'A
Theorem	dfdmf 4471*	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/_xA   &   |- F/_yA   =>   |- dom A = {x | E.y xAy }
Theorem	csbdmg 4472	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 4473*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- (A e. V -> (A e. dom B <-> E.y ABy))
Theorem	eldm2g 4474*	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 4475*	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 ABy)
Theorem	eldm2 4476*	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 4477	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- (A C_ B -> dom A C_ dom B)
Theorem	dmeq 4478	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|- (A = B -> dom A = dom B)
Theorem	dmeqi 4479	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|- A = B   =>   |- dom A = dom B
Theorem	dmeqd 4480	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|- (ph -> A = B)   =>   |- (ph -> dom A = dom B)
Theorem	opeldm 4481	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 4482	Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
|- A e. _V   &   |- B e. _V   =>   |- (A RB -> A e. dom R)
Theorem	opeldmg 4483	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 4484	Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
|- ((A e. C /\ B e. D /\ A RB) -> A e. dom R)
Theorem	dmun 4485	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 4486	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 4487	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 4488*	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 4489*	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.yph }
Theorem	dmopabss 4490*	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 4491*	The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
|- (A.x e. A E.yph <-> dom { <.x , y >. | (x e. A /\ ph) } = A)
Theorem	dm0 4492	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 4493	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 4494	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
|- dom _V = _V
Theorem	dm0rn0 4495	An empty domain implies an empty range. (Contributed by NM, 21-May-1998.)
|- ( dom A = (/) <-> ran A = (/))
Theorem	reldm0 4496	A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.)
|- ( Rel A -> (A = (/) <-> dom A = (/)))
Theorem	dmmrnm 4497*	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 4498*	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	dmxpinm 4499*	The domain of the intersection of two square cross products. Unlike dmin 4486, equality holds. (Contributed by NM, 29-Jan-2008.)
|- (E.x x e. (A i^i B) -> dom ((A X. A) i^i (B X. B)) = (A i^i B))
Theorem	xpid11m 4500*	The cross product of a class with itself is one-to-one. (Contributed by Jim Kingdon, 8-Dec-2018.)
|- ((E.x x e. A /\ E.x x e. B) -> ((A X. A) = (B X. B) <-> A = B))