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	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝑥 ⊆ 𝑦 → ∪ ( 𝐴 ∖ 𝐵 ) = ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		uniss2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ ( 𝐴 ∖ 𝐵 ) )
2		difss	⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴
3	2	unissi	⊢ ∪ ( 𝐴 ∖ 𝐵 ) ⊆ ∪ 𝐴
4	1 3	jctil	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝑥 ⊆ 𝑦 → ( ∪ ( 𝐴 ∖ 𝐵 ) ⊆ ∪ 𝐴 ∧ ∪ 𝐴 ⊆ ∪ ( 𝐴 ∖ 𝐵 ) ) )
5		eqss	⊢ ( ∪ ( 𝐴 ∖ 𝐵 ) = ∪ 𝐴 ↔ ( ∪ ( 𝐴 ∖ 𝐵 ) ⊆ ∪ 𝐴 ∧ ∪ 𝐴 ⊆ ∪ ( 𝐴 ∖ 𝐵 ) ) )
6	4 5	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) 𝑥 ⊆ 𝑦 → ∪ ( 𝐴 ∖ 𝐵 ) = ∪ 𝐴 )