Metamath Proof Explorer

Theorem difunieq

Description: The difference of unions is a subset of the union of the difference. (Contributed by ML, 29-Mar-2021)

Ref Expression
Assertion difunieq ( ∪ 𝐴 ∖ ∪ 𝐵 ) ⊆ ∪ ( 𝐴 ∖ 𝐵 )

Proof

Step Hyp Ref Expression
1 eluni ⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) )
2 eluni ⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )
3 2 notbii ⊢ ( ¬ 𝑥 ∈ ∪ 𝐵 ↔ ¬ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )
4 alinexa ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵 ) ↔ ¬ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )
5 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵 )
6 sp ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵 ) )
7 6 adantrd ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ¬ 𝑦 ∈ 𝐵 ) )
8 7 ancld ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
9 anass ⊢ ( ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
10 8 9 imbitrdi ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) ) )
11 5 10 eximd ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) ) )
12 4 11 sylbir ⊢ ( ¬ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) ) )
13 12 impcom ⊢ ( ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
14 1 3 13 syl2anb ⊢ ( ( 𝑥 ∈ ∪ 𝐴 ∧ ¬ 𝑥 ∈ ∪ 𝐵 ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
15 eldif ⊢ ( 𝑥 ∈ ( ∪ 𝐴 ∖ ∪ 𝐵 ) ↔ ( 𝑥 ∈ ∪ 𝐴 ∧ ¬ 𝑥 ∈ ∪ 𝐵 ) )
16 eluni ⊢ ( 𝑥 ∈ ∪ ( 𝐴 ∖ 𝐵 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ) )
17 eldif ⊢ ( 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) )
18 17 anbi2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
19 18 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∖ 𝐵 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
20 16 19 bitri ⊢ ( 𝑥 ∈ ∪ ( 𝐴 ∖ 𝐵 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
21 14 15 20 3imtr4i ⊢ ( 𝑥 ∈ ( ∪ 𝐴 ∖ ∪ 𝐵 ) → 𝑥 ∈ ∪ ( 𝐴 ∖ 𝐵 ) )
22 21 ssriv ⊢ ( ∪ 𝐴 ∖ ∪ 𝐵 ) ⊆ ∪ ( 𝐴 ∖ 𝐵 )