P. 40 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3901-4000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iuneq1 3901*	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 3902*	Equality theorem for restricted existential quantifier. (Contributed by NM, 27-Jun-1998.)
|- ( A = B -> |^|_ x e. A C = |^|_ x e. B C )
Theorem	ss2iun 3903	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 3904	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 3905	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 3906	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 3907	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 3908	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 3909*	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 3910*	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 3911*	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 3912*	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 3913*	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 3914*	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 3915*	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 3916*	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 3917*	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 3918	Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
|- F/_ x U_ x e. A B
Theorem	nfii1 3919	Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)
|- F/_ x |^|_ x e. A B
Theorem	dfiun2g 3920*	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 3921*	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 3922*	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 3923*	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 3924*	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 3925*	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 3926*	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 3927*	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 3928*	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 3929*	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 3930*	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 3931	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 3932*	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 3933*	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 3842. (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 3934*	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 3935*	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 3936*	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 3937*	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 3938	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 3939*	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 3940*	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 3941	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 3942*	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 3943*	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 3944*	An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
|- U_ x e. A { x } = A
Theorem	iun0 3945	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 3946	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 3947	An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.)
|- |^|_ x e. (/) A = _V
Theorem	viin 3948*	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 3949*	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 3950*	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 3951*	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 3952*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 3942 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 3953*	Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 3942 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 3954*	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 3955*	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 3956*	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 3957*	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 3958*	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 3959*	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 3960*	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 3961*	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 3962*	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 3963*	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 3964*	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 3965*	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 3966*	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 3967	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 3968	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 3969*	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 3970*	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 3971*	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 3972*	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 3973	Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
|- ( A C_ ~P B <-> U. A C_ B )
Theorem	pwssb 3974*	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 3975	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 3976*	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 }
Theorem	pwpwssunieq 3977*	The class of sets whose union is equal to a given class is included in the double power class of that class. (Contributed by BJ, 29-Apr-2021.)
|- { x | U. x = A } C_ ~P ~P A
Theorem	elpwuni 3978	Relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
|- ( B e. A -> ( A C_ ~P B <-> U. A = B ) )
Theorem	iinpw 3979*	The power class of an intersection in terms of indexed intersection. Exercise 24(a) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.)
|- ~P |^| A = |^|_ x e. A ~P x
Theorem	iunpwss 3980*	Inclusion of an indexed union of a power class in the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.)
|- U_ x e. A ~P x C_ ~P U. A
Theorem	rintm 3981*	Relative intersection of an inhabited class. (Contributed by Jim Kingdon, 19-Aug-2018.)
|- ( ( X C_ ~P A /\ E. x x e. X ) -> ( A i^i |^| X ) = |^| X )
2.1.21  Disjointness
Syntax	wdisj 3982	Extend wff notation to include the statement that a family of classes B ( x ), for x e. A, is a disjoint family.
wff Disj x e. A B
Definition	df-disj 3983*	A collection of classes B ( x ) is disjoint when for each element y, it is in B ( x ) for at most one x. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.)
|- (Disj x e. A B <-> A. y E* x e. A y e. B )
Theorem	dfdisj2 3984*	Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.)
|- (Disj x e. A B <-> A. y E* x ( x e. A /\ y e. B ) )
Theorem	disjss2 3985	If each element of a collection is contained in a disjoint collection, the original collection is also disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( A. x e. A B C_ C -> (Disj x e. A C -> Disj x e. A B ) )
Theorem	disjeq2 3986	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( A. x e. A B = C -> (Disj x e. A B <-> Disj x e. A C ) )
Theorem	disjeq2dv 3987*	Equality deduction for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> (Disj x e. A B <-> Disj x e. A C ) )
Theorem	disjss1 3988*	A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( A C_ B -> (Disj x e. B C -> Disj x e. A C ) )
Theorem	disjeq1 3989*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( A = B -> (Disj x e. A C <-> Disj x e. B C ) )
Theorem	disjeq1d 3990*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> (Disj x e. A C <-> Disj x e. B C ) )
Theorem	disjeq12d 3991*	Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> (Disj x e. A C <-> Disj x e. B D ) )
Theorem	cbvdisj 3992*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- (Disj x e. A B <-> Disj y e. A C )
Theorem	cbvdisjv 3993*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.)
|- ( x = y -> B = C )   =>    |- (Disj x e. A B <-> Disj y e. A C )
Theorem	nfdisjv 3994*	Bound-variable hypothesis builder for disjoint collection. (Contributed by Jim Kingdon, 19-Aug-2018.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/ yDisj x e. A B
Theorem	nfdisj1 3995	Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/ xDisj x e. A B
Theorem	disjnim 3996*	If a collection B ( i ) for i e. A is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Jim Kingdon, 6-Oct-2022.)
|- ( i = j -> B = C )   =>    |- (Disj i e. A B -> A. i e. A A. j e. A ( i =/= j -> ( B i^i C ) = (/) ) )
Theorem	disjnims 3997*	If a collection B ( i ) for i e. A is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by Jim Kingdon, 7-Oct-2022.)
|- (Disj x e. A B -> A. i e. A A. j e. A ( i =/= j -> ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
Theorem	disji2 3998*	Property of a disjoint collection: if B ( X ) = C and B ( Y ) = D, and X =/= Y, then C and D are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( x = X -> B = C )   &    |- ( x = Y -> B = D )   =>    |- ( (Disj x e. A B /\ ( X e. A /\ Y e. A ) /\ X =/= Y ) -> ( C i^i D ) = (/) )
Theorem	invdisj 3999*	If there is a function C ( y ) such that C ( y ) = x for all y e. B ( x ), then the sets B ( x ) for distinct x e. A are disjoint. (Contributed by Mario Carneiro, 10-Dec-2016.)
|- ( A. x e. A A. y e. B C = x -> Disj x e. A B )
Theorem	disjiun 4000*	A disjoint collection yields disjoint indexed unions for disjoint index sets. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.)
|- ( (Disj x e. A B /\ ( C C_ A /\ D C_ A /\ ( C i^i D ) = (/) ) ) -> ( U_ x e. C B i^i U_ x e. D B ) = (/) )