Theorem disjiunb

Description: Two ways to say that a collection of index unions C ( i , x ) for i e. A and x e. B is disjoint. (Contributed by AV, 9-Jan-2022)

	Ref	Expression
Hypotheses	disjiunb.1	|- ( i = j -> B = D )
	disjiunb.2	|- ( i = j -> C = E )
Assertion	disjiunb	|- ( Disj_ i e. A U_ x e. B C <-> A. i e. A A. j e. A ( i = j \/ ( U_ x e. B C i^i U_ x e. D E ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		disjiunb.1	|- ( i = j -> B = D )
2		disjiunb.2	|- ( i = j -> C = E )
3	1 2	iuneq12d	|- ( i = j -> U_ x e. B C = U_ x e. D E )
4	3	disjor	|- ( Disj_ i e. A U_ x e. B C <-> A. i e. A A. j e. A ( i = j \/ ( U_ x e. B C i^i U_ x e. D E ) = (/) ) )