Theorem undifr

Description: Union of complementary parts into whole. (Contributed by Thierry Arnoux, 21-Nov-2023)

	Ref	Expression
Assertion	undifr	|- ( A C_ B <-> ( ( B \ A ) u. A ) = B )

Proof

Step	Hyp	Ref	Expression
1		undif	|- ( A C_ B <-> ( A u. ( B \ A ) ) = B )
2		uncom	|- ( A u. ( B \ A ) ) = ( ( B \ A ) u. A )
3	2	eqeq1i	|- ( ( A u. ( B \ A ) ) = B <-> ( ( B \ A ) u. A ) = B )
4	1 3	bitri	|- ( A C_ B <-> ( ( B \ A ) u. A ) = B )