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\to B=D$$
	disjiunb.2	$$⊢i=j\to C=E$$
Assertion	disjiunb	$$⊢\underset{i\in A}{Disj}\bigcup _{x\in B}C\leftrightarrow \forall i\in A\forall j\in A\left(i=j\vee \bigcup _{x\in B}C\cap \bigcup _{x\in D}E=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		disjiunb.1	$$⊢i=j\to B=D$$
2		disjiunb.2	$$⊢i=j\to C=E$$
3	1 2	iuneq12d	$$⊢i=j\to \bigcup _{x\in B}C=\bigcup _{x\in D}E$$
4	3	disjor	$$⊢\underset{i\in A}{Disj}\bigcup _{x\in B}C\leftrightarrow \forall i\in A\forall j\in A\left(i=j\vee \bigcup _{x\in B}C\cap \bigcup _{x\in D}E=\varnothing \right)$$