P. 46 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4501-4600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unissint 4501	If the union of a class is included in its intersection, the class is either the empty set or a singleton (uniintsn 4514). (Contributed by NM, 30-Oct-2010.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( U. A C_ |^| A <-> ( A = (/) \/ U. A = |^| A ) )
Theorem	intssuni2 4502	Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006.)
|- ( ( A C_ B /\ A =/= (/) ) -> |^| A C_ U. B )
Theorem	intminss 4503*	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 4504*	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 4505*	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 4506*	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 4507*	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 7148 or abexssex 7149 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 4508	The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.)
|- ( (/) e. A -> |^| A = (/) )
Theorem	intun 4509	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 4510	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 4511	The intersection of a pair is the intersection of its members. Closed form of intpr 4510. 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 4512	Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( A e. V -> |^| { A } = A )
Theorem	intsn 4513	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 4514*	Two ways to express " A is a singleton." See also en1 8023, en1b 8024, card1 8794, and eusn 4265. (Contributed by NM, 2-Aug-2010.)
|- ( U. A = |^| A <-> E. x A = { x } )
Theorem	uniintab 4515	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 4516	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 4517	Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( X = (/) -> ( A i^i |^| X ) = A )
Theorem	elrint 4518*	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 4519*	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 4520	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 4436. While 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 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 4521	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 4475. 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 4522*	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 4554. Theorem uniiun 4573 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 6505 and funiunfv 6506 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 4523*	Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4522. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4555. Theorem intiin 4574 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 4524*	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 4525*	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	eliuni 4526*	Membership in an indexed union, one way. (Contributed by JJ, 27-Jul-2021.)
|- ( x = A -> B = C )   =>    |- ( ( A e. D /\ E e. C ) -> E e. U_ x e. D B )
Theorem	iuncom 4527*	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 4528	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 4529*	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 4530*	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 4531*	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 4532*	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 4533*	Subclass theorem for indexed intersection. (Contributed by NM, 24-Jan-2012.)
|- ( A C_ B -> |^|_ x e. B C C_ |^|_ x e. A C )
Theorem	iuneq1 4534*	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 4535*	Equality theorem for indexed intersection. (Contributed by NM, 27-Jun-1998.)
|- ( A = B -> |^|_ x e. A C = |^|_ x e. B C )
Theorem	ss2iun 4536	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 4537	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 4538	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 4539	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 4540	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 4541	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 4542*	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 4543*	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	iuneq12df 4544	Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x B   &    |- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> U_ x e. A C = U_ x e. B D )
Theorem	iuneq1d 4545*	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 4546*	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 4547*	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 4548	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 4549	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 4550	Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
|- F/_ x U_ x e. A B
Theorem	nfii1 4551	Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
|- F/_ x |^|_ x e. A B
Theorem	dfiun2g 4552*	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 4553*	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 4554*	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 4555*	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 4556*	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 4557*	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 4558*	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 4559*	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 4560*	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 4561*	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 4562*	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 4563	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 4564*	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 4565*	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 4470. (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 4566*	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 4567*	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 4568*	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 4569	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 4570*	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 4571*	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 4572	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 4573*	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 4574*	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 4575*	An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
|- U_ x e. A { x } = A
Theorem	iun0 4576	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 4577	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 4578	An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.)
|- |^|_ x e. (/) A = _V
Theorem	viin 4579*	Indexed intersection with a universal index class. When A doesn't depend on x, this evaluates to A by 19.3 2069 and abid2 2745. When A = x, this evaluates to (/) by intiin 4574 and intv 4841. (Contributed by NM, 11-Sep-2008.)
|- |^|_ x e. _V A = { y | A. x y e. A }
Theorem	iunn0 4580*	There is a nonempty class in an indexed collection B ( x ) iff the indexed union of them is nonempty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( E. x e. A B =/= (/) <-> U_ x e. A B =/= (/) )
Theorem	iinab 4581*	Indexed intersection of a class builder. (Contributed by NM, 6-Dec-2011.)
|- |^|_ x e. A { y | ph } = { y | A. x e. A ph }
Theorem	iinrab 4582*	Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)
|- ( A =/= (/) -> |^|_ x e. A { y e. B | ph } = { y e. B | A. x e. A ph } )
Theorem	iinrab2 4583*	Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)
|- ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph }
Theorem	iunin2 4584*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4573 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 4585*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4573 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	iinun2 4586*	Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4574 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
|- |^|_ x e. A ( B u. C ) = ( B u. |^|_ x e. A C )
Theorem	iundif2 4587*	Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 4574 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
|- U_ x e. A ( B \ C ) = ( B \ |^|_ x e. A C )
Theorem	2iunin 4588*	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	iindif2 4589*	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 4573 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.)
|- ( A =/= (/) -> |^|_ x e. A ( B \ C ) = ( B \ U_ x e. A C ) )
Theorem	iinin2 4590*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4574 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( A =/= (/) -> |^|_ x e. A ( B i^i C ) = ( B i^i |^|_ x e. A C ) )
Theorem	iinin1 4591*	Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4574 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( A =/= (/) -> |^|_ x e. A ( C i^i B ) = ( |^|_ x e. A C i^i B ) )
Theorem	iinvdif 4592*	The indexed intersection of a complement. (Contributed by Gérard Lang, 5-Aug-2018.)
|- |^|_ x e. A ( _V \ B ) = ( _V \ U_ x e. A B )
Theorem	elriin 4593*	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 4594*	Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( X = (/) -> ( A i^i |^|_ x e. X S ) = A )
Theorem	riinn0 4595*	Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( ( A. x e. X S C_ A /\ X =/= (/) ) -> ( A i^i |^|_ x e. X S ) = |^|_ x e. X S )
Theorem	riinrab 4596*	Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.)
|- ( A i^i |^|_ x e. X { y e. A | ph } ) = { y e. A | A. x e. X ph }
Theorem	symdif0 4597	Symmetric difference with the empty class. (Contributed by Scott Fenton, 24-Apr-2012.)
|- ( A /_\ (/) ) = A
Theorem	symdifv 4598	Symmetric difference with the universal class. (Contributed by Scott Fenton, 24-Apr-2012.)
|- ( A /_\ _V ) = ( _V \ A )
Theorem	symdifid 4599	Symmetric difference with self yields the empty class. (Contributed by Scott Fenton, 25-Apr-2012.)
|- ( A /_\ A ) = (/)
Theorem	iinxsng 4600*	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 )