P. 41 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4001-4100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	intun 4001	The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. (Contributed by NM, 22-Sep-2002.)
|- |^| ( A u. B ) = ( |^| A i^i |^| B )
Theorem	intpr 4002	The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42. (Contributed by NM, 14-Oct-1999.)
|- A e. _V   &    |- B e. _V   =>    |- |^| { A , B } = ( A i^i B )
Theorem	intprg 4003	The intersection of a pair is the intersection of its members. Closed form of intpr 4002. Theorem 71 of [Suppes] p. 42. (Contributed by FL, 27-Apr-2008.)
|- ( ( A e. V /\ B e. W ) -> |^| { A , B } = ( A i^i B ) )
Theorem	intsng 4004	Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( A e. V -> |^| { A } = A )
Theorem	intsn 4005	The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41. (Contributed by NM, 29-Sep-2002.)
|- A e. _V   =>    |- |^| { A } = A
Theorem	uniintsnr 4006*	The union and intersection of a singleton are equal. See also eusn 3785. (Contributed by Jim Kingdon, 14-Aug-2018.)
|- ( E. x A = { x } -> U. A = |^| A )
Theorem	uniintabim 4007	The union and the intersection of a class abstraction are equal if there is a unique satisfying value of ph ( x ). (Contributed by Jim Kingdon, 14-Aug-2018.)
|- ( E! x ph -> U. { x | ph } = |^| { x | ph } )
Theorem	intunsn 4008	Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002.)
|- B e. _V   =>    |- |^| ( A u. { B } ) = ( |^| A i^i B )
Theorem	rint0 4009	Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( X = (/) -> ( A i^i |^| X ) = A )
Theorem	elrint 4010*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( X e. ( A i^i |^| B ) <-> ( X e. A /\ A. y e. B X e. y ) )
Theorem	elrint2 4011*	Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( X e. A -> ( X e. ( A i^i |^| B ) <-> A. y e. B X e. y ) )
2.1.20  Indexed union and intersection
Syntax	ciun 4012	Extend class notation to include indexed union. Note: Historically (prior to 21-Oct-2005), set.mm used the notation U. x e. A B, with the same union symbol as cuni 3935. While that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses as distinguished symbol U_ instead of U. and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
class U_ x e. A B
Syntax	ciin 4013	Extend class notation to include indexed intersection. Note: Historically (prior to 21-Oct-2005), set.mm used the notation |^| x e. A B, with the same intersection symbol as cint 3970. Although that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses a distinguished symbol |^|_ instead of |^| and does allow LALR parsing. Thanks to Peter Backes for suggesting this change.
class |^|_ x e. A B
Definition	df-iun 4014*	Define indexed union. Definition indexed union in [Stoll] p. 45. In most applications, A is independent of x (although this is not required by the definition), and B depends on x i.e. can be read informally as B ( x ). We call x the index, A the index set, and B the indexed set. In most books, x e. A is written as a subscript or underneath a union symbol U.. We use a special union symbol U_ to make it easier to distinguish from plain class union. In many theorems, you will see that x and A are in the same disjoint variable group (meaning A cannot depend on x) and that B and x do not share a disjoint variable group (meaning that can be thought of as B ( x ) i.e. can be substituted with a class expression containing x). An alternate definition tying indexed union to ordinary union is dfiun2 4046. Theorem uniiun 4066 provides a definition of ordinary union in terms of indexed union. (Contributed by NM, 27-Jun-1998.)
|- U_ x e. A B = { y | E. x e. A y e. B }
Definition	df-iin 4015*	Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4014. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4047. Theorem intiin 4067 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.)
|- |^|_ x e. A B = { y | A. x e. A y e. B }
Theorem	eliun 4016*	Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
|- ( A e. U_ x e. B C <-> E. x e. B A e. C )
Theorem	eliin 4017*	Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
|- ( A e. V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
Theorem	iuncom 4018*	Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
|- U_ x e. A U_ y e. B C = U_ y e. B U_ x e. A C
Theorem	iuncom4 4019	Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014.)
|- U_ x e. A U. B = U. U_ x e. A B
Theorem	iunconstm 4020*	Indexed union of a constant class, i.e. where B does not depend on x. (Contributed by Jim Kingdon, 15-Aug-2018.)
|- ( E. x x e. A -> U_ x e. A B = B )
Theorem	iinconstm 4021*	Indexed intersection of a constant class, i.e. where B does not depend on x. (Contributed by Jim Kingdon, 19-Dec-2018.)
|- ( E. y y e. A -> |^|_ x e. A B = B )
Theorem	iuniin 4022*	Law combining indexed union with indexed intersection. Eq. 14 in [KuratowskiMostowski] p. 109. This theorem also appears as the last example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- U_ x e. A |^|_ y e. B C C_ |^|_ y e. B U_ x e. A C
Theorem	iunss1 4023*	Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A C_ B -> U_ x e. A C C_ U_ x e. B C )
Theorem	iinss1 4024*	Subclass theorem for indexed union. (Contributed by NM, 24-Jan-2012.)
|- ( A C_ B -> |^|_ x e. B C C_ |^|_ x e. A C )
Theorem	iuneq1 4025*	Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)
|- ( A = B -> U_ x e. A C = U_ x e. B C )
Theorem	iineq1 4026*	Equality theorem for restricted existential quantifier. (Contributed by NM, 27-Jun-1998.)
|- ( A = B -> |^|_ x e. A C = |^|_ x e. B C )
Theorem	ss2iun 4027	Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A. x e. A B C_ C -> U_ x e. A B C_ U_ x e. A C )
Theorem	iuneq2 4028	Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.)
|- ( A. x e. A B = C -> U_ x e. A B = U_ x e. A C )
Theorem	iineq2 4029	Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A. x e. A B = C -> |^|_ x e. A B = |^|_ x e. A C )
Theorem	iuneq2i 4030	Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.)
|- ( x e. A -> B = C )   =>    |- U_ x e. A B = U_ x e. A C
Theorem	iineq2i 4031	Equality inference for indexed intersection. (Contributed by NM, 22-Oct-2003.)
|- ( x e. A -> B = C )   =>    |- |^|_ x e. A B = |^|_ x e. A C
Theorem	iineq2d 4032	Equality deduction for indexed intersection. (Contributed by NM, 7-Dec-2011.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> |^|_ x e. A B = |^|_ x e. A C )
Theorem	iuneq2dv 4033*	Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> U_ x e. A B = U_ x e. A C )
Theorem	iineq2dv 4034*	Equality deduction for indexed intersection. (Contributed by NM, 3-Aug-2004.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> |^|_ x e. A B = |^|_ x e. A C )
Theorem	iuneq1d 4035*	Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
|- ( ph -> A = B )   =>    |- ( ph -> U_ x e. A C = U_ x e. B C )
Theorem	iuneq12d 4036*	Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> U_ x e. A C = U_ x e. B D )
Theorem	iuneq2d 4037*	Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)
|- ( ph -> B = C )   =>    |- ( ph -> U_ x e. A B = U_ x e. A C )
Theorem	nfiunxy 4038*	Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/_ y U_ x e. A B
Theorem	nfiinxy 4039*	Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/_ y |^|_ x e. A B
Theorem	nfiunya 4040*	Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/_ y U_ x e. A B
Theorem	nfiinya 4041*	Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/_ y |^|_ x e. A B
Theorem	nfiu1 4042	Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
|- F/_ x U_ x e. A B
Theorem	nfii1 4043	Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
|- F/_ x |^|_ x e. A B
Theorem	dfiun2g 4044*	Alternate definition of indexed union when B is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A. x e. A B e. C -> U_ x e. A B = U. { y | E. x e. A y = B } )
Theorem	dfiin2g 4045*	Alternate definition of indexed intersection when B is a set. (Contributed by Jeff Hankins, 27-Aug-2009.)
|- ( A. x e. A B e. C -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )
Theorem	dfiun2 4046*	Alternate definition of indexed union when B is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.)
|- B e. _V   =>    |- U_ x e. A B = U. { y | E. x e. A y = B }
Theorem	dfiin2 4047*	Alternate definition of indexed intersection when B is a set. Definition 15(b) of [Suppes] p. 44. (Contributed by NM, 28-Jun-1998.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- B e. _V   =>    |- |^|_ x e. A B = |^| { y | E. x e. A y = B }
Theorem	dfiunv2 4048*	Define double indexed union. (Contributed by FL, 6-Nov-2013.)
|- U_ x e. A U_ y e. B C = { z | E. x e. A E. y e. B z e. C }
Theorem	cbviun 4049*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.)
|- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- U_ x e. A B = U_ y e. A C
Theorem	cbviin 4050*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- |^|_ x e. A B = |^|_ y e. A C
Theorem	cbviunv 4051*	Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.)
|- ( x = y -> B = C )   =>    |- U_ x e. A B = U_ y e. A C
Theorem	cbviinv 4052*	Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.)
|- ( x = y -> B = C )   =>    |- |^|_ x e. A B = |^|_ y e. A C
Theorem	iunss 4053*	Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( U_ x e. A B C_ C <-> A. x e. A B C_ C )
Theorem	ssiun 4054*	Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( E. x e. A C C_ B -> C C_ U_ x e. A B )
Theorem	ssiun2 4055	Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( x e. A -> B C_ U_ x e. A B )
Theorem	ssiun2s 4056*	Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
|- ( x = C -> B = D )   =>    |- ( C e. A -> D C_ U_ x e. A B )
Theorem	iunss2 4057*	A subclass condition on the members of two indexed classes C ( x ) and D ( y ) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59. Compare uniss2 3966. (Contributed by NM, 9-Dec-2004.)
|- ( A. x e. A E. y e. B C C_ D -> U_ x e. A C C_ U_ y e. B D )
Theorem	iunssd 4058*	Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ( ph /\ x e. A ) -> B C_ C )   =>    |- ( ph -> U_ x e. A B C_ C )
Theorem	iunab 4059*	The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.)
|- U_ x e. A { y | ph } = { y | E. x e. A ph }
Theorem	iunrab 4060*	The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|- U_ x e. A { y e. B | ph } = { y e. B | E. x e. A ph }
Theorem	iunxdif2 4061*	Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004.)
|- ( x = y -> C = D )   =>    |- ( A. x e. A E. y e. ( A \ B ) C C_ D -> U_ y e. ( A \ B ) D = U_ x e. A C )
Theorem	ssiinf 4062	Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
|- F/_ x C   =>    |- ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )
Theorem	ssiin 4063*	Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003.)
|- ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )
Theorem	iinss 4064*	Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )
Theorem	iinss2 4065	An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.)
|- ( x e. A -> |^|_ x e. A B C_ B )
Theorem	uniiun 4066*	Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.)
|- U. A = U_ x e. A x
Theorem	intiin 4067*	Class intersection in terms of indexed intersection. Definition in [Stoll] p. 44. (Contributed by NM, 28-Jun-1998.)
|- |^| A = |^|_ x e. A x
Theorem	iunid 4068*	An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
|- U_ x e. A { x } = A
Theorem	iun0 4069	An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- U_ x e. A (/) = (/)
Theorem	0iun 4070	An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- U_ x e. (/) A = (/)
Theorem	0iin 4071	An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.)
|- |^|_ x e. (/) A = _V
Theorem	viin 4072*	Indexed intersection with a universal index class. (Contributed by NM, 11-Sep-2008.)
|- |^|_ x e. _V A = { y | A. x y e. A }
Theorem	iunn0m 4073*	There is an inhabited class in an indexed collection B ( x ) iff the indexed union of them is inhabited. (Contributed by Jim Kingdon, 16-Aug-2018.)
|- ( E. x e. A E. y y e. B <-> E. y y e. U_ x e. A B )
Theorem	iinab 4074*	Indexed intersection of a class builder. (Contributed by NM, 6-Dec-2011.)
|- |^|_ x e. A { y | ph } = { y | A. x e. A ph }
Theorem	iinrabm 4075*	Indexed intersection of a restricted class builder. (Contributed by Jim Kingdon, 16-Aug-2018.)
|- ( E. x x e. A -> |^|_ x e. A { y e. B | ph } = { y e. B | A. x e. A ph } )
Theorem	iunin2 4076*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4066 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
|- U_ x e. A ( B i^i C ) = ( B i^i U_ x e. A C )
Theorem	iunin1 4077*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4066 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- U_ x e. A ( C i^i B ) = ( U_ x e. A C i^i B )
Theorem	iundif2ss 4078*	Indexed union of class difference. Compare to theorem "De Morgan's laws" in [Enderton] p. 31. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- U_ x e. A ( B \ C ) C_ ( B \ |^|_ x e. A C )
Theorem	2iunin 4079*	Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.)
|- U_ x e. A U_ y e. B ( C i^i D ) = ( U_ x e. A C i^i U_ y e. B D )
Theorem	iindif2m 4080*	Indexed intersection of class difference. Compare to Theorem "De Morgan's laws" in [Enderton] p. 31. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- ( E. x x e. A -> |^|_ x e. A ( B \ C ) = ( B \ U_ x e. A C ) )
Theorem	iinin2m 4081*	Indexed intersection of intersection. Compare to Theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- ( E. x x e. A -> |^|_ x e. A ( B i^i C ) = ( B i^i |^|_ x e. A C ) )
Theorem	iinin1m 4082*	Indexed intersection of intersection. Compare to Theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- ( E. x x e. A -> |^|_ x e. A ( C i^i B ) = ( |^|_ x e. A C i^i B ) )
Theorem	elriin 4083*	Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( B e. ( A i^i |^|_ x e. X S ) <-> ( B e. A /\ A. x e. X B e. S ) )
Theorem	riin0 4084*	Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( X = (/) -> ( A i^i |^|_ x e. X S ) = A )
Theorem	riinm 4085*	Relative intersection of an inhabited family. (Contributed by Jim Kingdon, 19-Aug-2018.)
|- ( ( A. x e. X S C_ A /\ E. x x e. X ) -> ( A i^i |^|_ x e. X S ) = |^|_ x e. X S )
Theorem	iinxsng 4086*	A singleton index picks out an instance of an indexed intersection's argument. (Contributed by NM, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- ( x = A -> B = C )   =>    |- ( A e. V -> |^|_ x e. { A } B = C )
Theorem	iinxprg 4087*	Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.)
|- ( x = A -> C = D )   &    |- ( x = B -> C = E )   =>    |- ( ( A e. V /\ B e. W ) -> |^|_ x e. { A , B } C = ( D i^i E ) )
Theorem	iunxsng 4088*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.)
|- ( x = A -> B = C )   =>    |- ( A e. V -> U_ x e. { A } B = C )
Theorem	iunxsn 4089*	A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 25-Jun-2016.)
|- A e. _V   &    |- ( x = A -> B = C )   =>    |- U_ x e. { A } B = C
Theorem	iunxsngf 4090*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) (Revised by Thierry Arnoux, 2-May-2020.)
|- F/_ x C   &    |- ( x = A -> B = C )   =>    |- ( A e. V -> U_ x e. { A } B = C )
Theorem	iunun 4091	Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- U_ x e. A ( B u. C ) = ( U_ x e. A B u. U_ x e. A C )
Theorem	iunxun 4092	Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- U_ x e. ( A u. B ) C = ( U_ x e. A C u. U_ x e. B C )
Theorem	iunxprg 4093*	A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
|- ( x = A -> C = D )   &    |- ( x = B -> C = E )   =>    |- ( ( A e. V /\ B e. W ) -> U_ x e. { A , B } C = ( D u. E ) )
Theorem	iunxiun 4094*	Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.)
|- U_ x e. U_ y e. A B C = U_ y e. A U_ x e. B C
Theorem	iinuniss 4095*	A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33 but with equality changed to subset. (Contributed by Jim Kingdon, 19-Aug-2018.)
|- ( A u. |^| B ) C_ |^|_ x e. B ( A u. x )
Theorem	iununir 4096*	A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33 but with biconditional changed to implication. (Contributed by Jim Kingdon, 19-Aug-2018.)
|- ( ( A u. U. B ) = U_ x e. B ( A u. x ) -> ( B = (/) -> A = (/) ) )
Theorem	sspwuni 4097	Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
|- ( A C_ ~P B <-> U. A C_ B )
Theorem	pwssb 4098*	Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.)
|- ( A C_ ~P B <-> A. x e. A x C_ B )
Theorem	elpwpw 4099	Characterization of the elements of a double power class: they are exactly the sets whose union is included in that class. (Contributed by BJ, 29-Apr-2021.)
|- ( A e. ~P ~P B <-> ( A e. _V /\ U. A C_ B ) )
Theorem	pwpwab 4100*	The double power class written as a class abstraction: the class of sets whose union is included in the given class. (Contributed by BJ, 29-Apr-2021.)
|- ~P ~P A = { x | U. x C_ A }