Theorem unidif

Description: If the difference A \ B contains the largest members of A , then the union of the difference is the union of A . (Contributed by NM, 22-Mar-2004)

	Ref	Expression
Assertion	unidif	|- ( A. x e. A E. y e. ( A \ B ) x C_ y -> U. ( A \ B ) = U. A )

Proof

Step	Hyp	Ref	Expression
1		uniss2	|- ( A. x e. A E. y e. ( A \ B ) x C_ y -> U. A C_ U. ( A \ B ) )
2		difss	|- ( A \ B ) C_ A
3	2	unissi	|- U. ( A \ B ) C_ U. A
4	1 3	jctil	|- ( A. x e. A E. y e. ( A \ B ) x C_ y -> ( U. ( A \ B ) C_ U. A /\ U. A C_ U. ( A \ B ) ) )
5		eqss	|- ( U. ( A \ B ) = U. A <-> ( U. ( A \ B ) C_ U. A /\ U. A C_ U. ( A \ B ) ) )
6	4 5	sylibr	|- ( A. x e. A E. y e. ( A \ B ) x C_ y -> U. ( A \ B ) = U. A )