P. 41 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 4001-4100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uni0c 4001*	The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.)
|- ( U. A = (/) <-> A. x e. A x = (/) )
Theorem	uni0 4002	The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4298 by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)
|- U. (/) = (/)
Theorem	elssuni 4003	An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)
|- ( A e. B -> A C_ U. B )
Theorem	unissel 4004	Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.)
|- ( ( U. A C_ B /\ B e. A ) -> U. A = B )
Theorem	unissb 4005*	Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)
|- ( U. A C_ B <-> A. x e. A x C_ B )
Theorem	uniss2 4006*	A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. See iunss2 4096 for a generalization to indexed unions. (Contributed by NM, 22-Mar-2004.)
|- ( A. x e. A E. y e. B x C_ y -> U. A C_ U. B )
Theorem	unidif 4007*	If the difference A \ B contains the largest members of A, then the union of the difference is the union of A. (Contributed by NM, 22-Mar-2004.)
|- ( A. x e. A E. y e. ( A \ B ) x C_ y -> U. ( A \ B ) = U. A )
Theorem	ssunieq 4008*	Relationship implying union. (Contributed by NM, 10-Nov-1999.)
|- ( ( A e. B /\ A. x e. B x C_ A ) -> A = U. B )
Theorem	unimax 4009*	Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002.)
|- ( A e. B -> U. { x e. B | x C_ A } = A )
2.1.19  The intersection of a class
Syntax	cint 4010	Extend class notation to include the intersection of a class (read: 'intersect A').
class |^| A
Definition	df-int 4011*	Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44. For example, |^| { { 1 , 3 } , { 1 , 8 } } = { 1 }. Compare this with the intersection of two classes, df-in 3287. (Contributed by NM, 18-Aug-1993.)
|- |^| A = { x | A. y ( y e. A -> x e. y ) }
Theorem	dfint2 4012*	Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.)
|- |^| A = { x | A. y e. A x e. y }
Theorem	inteq 4013	Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
|- ( A = B -> |^| A = |^| B )
Theorem	inteqi 4014	Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
|- A = B   =>    |- |^| A = |^| B
Theorem	inteqd 4015	Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
|- ( ph -> A = B )   =>    |- ( ph -> |^| A = |^| B )
Theorem	elint 4016*	Membership in class intersection. (Contributed by NM, 21-May-1994.)
|- A e. _V   =>    |- ( A e. |^| B <-> A. x ( x e. B -> A e. x ) )
Theorem	elint2 4017*	Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
|- A e. _V   =>    |- ( A e. |^| B <-> A. x e. B A e. x )
Theorem	elintg 4018*	Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.)
|- ( A e. V -> ( A e. |^| B <-> A. x e. B A e. x ) )
Theorem	elinti 4019	Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A e. |^| B -> ( C e. B -> A e. C ) )
Theorem	nfint 4020	Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- F/_ x A   =>    |- F/_ x |^| A
Theorem	elintab 4021*	Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
|- A e. _V   =>    |- ( A e. |^| { x | ph } <-> A. x ( ph -> A e. x ) )
Theorem	elintrab 4022*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
|- A e. _V   =>    |- ( A e. |^| { x e. B | ph } <-> A. x e. B ( ph -> A e. x ) )
Theorem	elintrabg 4023*	Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.)
|- ( A e. V -> ( A e. |^| { x e. B | ph } <-> A. x e. B ( ph -> A e. x ) ) )
Theorem	int0 4024	The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.)
|- |^| (/) = _V
Theorem	intss1 4025	An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.)
|- ( A e. B -> |^| B C_ A )
Theorem	ssint 4026*	Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
|- ( A C_ |^| B <-> A. x e. B A C_ x )
Theorem	ssintab 4027*	Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A C_ |^| { x | ph } <-> A. x ( ph -> A C_ x ) )
Theorem	ssintub 4028*	Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
|- A C_ |^| { x e. B | A C_ x }
Theorem	ssmin 4029*	Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.)
|- A C_ |^| { x | ( A C_ x /\ ph ) }
Theorem	intmin 4030*	Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A e. B -> |^| { x e. B | A C_ x } = A )
Theorem	intss 4031	Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
|- ( A C_ B -> |^| B C_ |^| A )
Theorem	intssuni 4032	The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
|- ( A =/= (/) -> |^| A C_ U. A )
Theorem	ssintrab 4033*	Subclass of the intersection of a restricted class builder. (Contributed by NM, 30-Jan-2015.)
|- ( A C_ |^| { x e. B | ph } <-> A. x e. B ( ph -> A C_ x ) )
Theorem	unissint 4034	If the union of a class is included in its intersection, the class is either the empty set or a singleton (uniintsn 4047). (Contributed by NM, 30-Oct-2010.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( U. A C_ |^| A <-> ( A = (/) \/ U. A = |^| A ) )
Theorem	intssuni2 4035	Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006.)
|- ( ( A C_ B /\ A =/= (/) ) -> |^| A C_ U. B )
Theorem	intminss 4036*	Under subset ordering, the intersection of a restricted class abstraction is less than or equal to any of its members. (Contributed by NM, 7-Sep-2013.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( ( A e. B /\ ps ) -> |^| { x e. B | ph } C_ A )
Theorem	intmin2 4037*	Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003.)
|- A e. _V   =>    |- |^| { x | A C_ x } = A
Theorem	intmin3 4038*	Under subset ordering, the intersection of a class abstraction is less than or equal to any of its members. (Contributed by NM, 3-Jul-2005.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ps   =>    |- ( A e. V -> |^| { x | ph } C_ A )
Theorem	intmin4 4039*	Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006.)
|- ( A C_ |^| { x | ph } -> |^| { x | ( A C_ x /\ ph ) } = |^| { x | ph } )
Theorem	intab 4040*	The intersection of a special case of a class abstraction. y may be free in ph and A, which can be thought of a ph ( y ) and A ( y ). Typically, abrexex2 5960 or abexssex 5961 can be used to satisfy the second hypothesis. (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|- A e. _V   &    |- { x | E. y ( ph /\ x = A ) } e. _V   =>    |- |^| { x | A. y ( ph -> A e. x ) } = { x | E. y ( ph /\ x = A ) }
Theorem	int0el 4041	The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.)
|- ( (/) e. A -> |^| A = (/) )
Theorem	intun 4042	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 4043	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 4044	The intersection of a pair is the intersection of its members. Closed form of intpr 4043. 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 4045	Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( A e. V -> |^| { A } = A )
Theorem	intsn 4046	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	uniintsn 4047*	Two ways to express " A is a singleton." See also en1 7133, en1b 7134, card1 7811, and eusn 3840. (Contributed by NM, 2-Aug-2010.)
|- ( U. A = |^| A <-> E. x A = { x } )
Theorem	uniintab 4048	The union and the intersection of a class abstraction are equal exactly when there is a unique satisfying value of ph ( x ). (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( E! x ph <-> U. { x | ph } = |^| { x | ph } )
Theorem	intunsn 4049	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 4050	Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( X = (/) -> ( A i^i |^| X ) = A )
Theorem	elrint 4051*	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 4052*	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 4053	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 3975. 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 4054	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 4010. 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 4055*	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 distinct variable group (meaning A cannot depend on x) and that B and x do not share a distinct 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 4085. Theorem uniiun 4104 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 5953 and funiunfv 5954 are useful when B is a function. (Contributed by NM, 27-Jun-1998.)
|- U_ x e. A B = { y | E. x e. A y e. B }
Definition	df-iin 4056*	Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4055. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4086. Theorem intiin 4105 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 4057*	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 4058*	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 4059*	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 4060	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	iunconst 4061*	Indexed union of a constant class, i.e. where B does not depend on x. (Contributed by NM, 5-Sep-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A =/= (/) -> U_ x e. A B = B )
Theorem	iinconst 4062*	Indexed intersection of a constant class, i.e. where B does not depend on x. (Contributed by Mario Carneiro, 6-Feb-2015.)
|- ( A =/= (/) -> |^|_ x e. A B = B )
Theorem	iuniin 4063*	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 4064*	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 4065*	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 4066*	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 4067*	Equality theorem for restricted existential quantifier. (Contributed by NM, 27-Jun-1998.)
|- ( A = B -> |^|_ x e. A C = |^|_ x e. B C )
Theorem	ss2iun 4068	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 4069	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 4070	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 4071	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 4072	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 4073	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 4074*	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 4075*	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 4076*	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 4077*	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 4078*	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	nfiun 4079	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	nfiin 4080	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 4081	Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
|- F/_ x U_ x e. A B
Theorem	nfii1 4082	Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
|- F/_ x |^|_ x e. A B
Theorem	dfiun2g 4083*	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 4084*	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 4085*	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 4086*	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 4087*	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 4088*	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 4089*	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 4090*	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 4091*	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 4092*	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 4093*	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 4094	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 4095*	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 4096*	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 4006. (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	iunab 4097*	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 4098*	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 4099*	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 4100	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 )