Theorem undifrOLD

Description: Obsolete version of undifr as of 11-Mar-2025. (Contributed by Thierry Arnoux, 21-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	undifrOLD	|- ( 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 )