Theorem undisj1

Description: The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004)

	Ref	Expression
Assertion	undisj1	|- ( ( ( A i^i C ) = (/) /\ ( B i^i C ) = (/) ) <-> ( ( A u. B ) i^i C ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		un00	|- ( ( ( A i^i C ) = (/) /\ ( B i^i C ) = (/) ) <-> ( ( A i^i C ) u. ( B i^i C ) ) = (/) )
2		indir	|- ( ( A u. B ) i^i C ) = ( ( A i^i C ) u. ( B i^i C ) )
3	2	eqeq1i	|- ( ( ( A u. B ) i^i C ) = (/) <-> ( ( A i^i C ) u. ( B i^i C ) ) = (/) )
4	1 3	bitr4i	|- ( ( ( A i^i C ) = (/) /\ ( B i^i C ) = (/) ) <-> ( ( A u. B ) i^i C ) = (/) )