![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssundif | Structured version Visualization version GIF version |
Description: A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.) |
Ref | Expression |
---|---|
ssundif | ⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.6 1000 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) | |
2 | eldif 3920 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 2 | imbi1i 349 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶)) |
4 | elun 4108 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
5 | 4 | imbi2i 335 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
6 | 1, 3, 5 | 3bitr4ri 303 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶)) |
7 | 6 | albii 1821 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶)) |
8 | dfss2 3930 | . 2 ⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶))) | |
9 | dfss2 3930 | . 2 ⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶)) | |
10 | 7, 8, 9 | 3bitr4i 302 | 1 ⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∀wal 1539 ∈ wcel 2106 ∖ cdif 3907 ∪ cun 3908 ⊆ wss 3910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 |
This theorem is referenced by: difcom 4446 uneqdifeq 4450 ssunsn2 4787 elpwun 7703 soex 7858 ressuppssdif 8116 ssfi 9117 frfi 9232 cantnfp1lem3 9616 dfacfin7 10335 zornn0g 10441 fpwwe2lem12 10578 hashbclem 14349 incexclem 15721 ramub1lem1 16898 lpcls 22715 cmpcld 22753 alexsubALTlem3 23400 restmetu 23926 uniiccdif 24942 abelthlem2 25791 abelthlem3 25792 pmtrcnelor 31942 imadifss 36053 frege124d 42023 |
Copyright terms: Public domain | W3C validator |