Theorem disjuniel

Description: A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020)

	Ref	Expression
Hypotheses	disjuniel.1	$$⊢\phi \to \underset{x\in A}{Disj}x$$
	disjuniel.2	$$⊢\phi \to B\subseteq A$$
	disjuniel.3	$$⊢\phi \to C\in \left(A\setminus B\right)$$
Assertion	disjuniel	$$⊢\phi \to \bigcup B\cap C=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		disjuniel.1	$$⊢\phi \to \underset{x\in A}{Disj}x$$
2		disjuniel.2	$$⊢\phi \to B\subseteq A$$
3		disjuniel.3	$$⊢\phi \to C\in \left(A\setminus B\right)$$
4		uniiun	$$⊢\bigcup B=\bigcup _{x\in B}x$$
5	4	ineq1i	$$⊢\bigcup B\cap C=\bigcup _{x\in B}x\cap C$$
6		id	$$⊢x=C\to x=C$$
7	1 6 2 3	disjiunel	$$⊢\phi \to \bigcup _{x\in B}x\cap C=\varnothing$$
8	5 7	syl5eq	$$⊢\phi \to \bigcup B\cap C=\varnothing$$