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	|- ( ph -> Disj_ x e. A x )
	disjuniel.2	|- ( ph -> B C_ A )
	disjuniel.3	|- ( ph -> C e. ( A \ B ) )
Assertion	disjuniel	|- ( ph -> ( U. B i^i C ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		disjuniel.1	|- ( ph -> Disj_ x e. A x )
2		disjuniel.2	|- ( ph -> B C_ A )
3		disjuniel.3	|- ( ph -> C e. ( A \ B ) )
4		uniiun	|- U. B = U_ x e. B x
5	4	ineq1i	|- ( U. B i^i C ) = ( U_ x e. B x i^i C )
6		id	|- ( x = C -> x = C )
7	1 6 2 3	disjiunel	|- ( ph -> ( U_ x e. B x i^i C ) = (/) )
8	5 7	syl5eq	|- ( ph -> ( U. B i^i C ) = (/) )