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 1002 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) | |
2 | eldif 3876 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 2 | imbi1i 353 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶)) |
4 | elun 4063 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
5 | 4 | imbi2i 339 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
6 | 1, 3, 5 | 3bitr4ri 307 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶)) |
7 | 6 | albii 1827 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶)) |
8 | dfss2 3886 | . 2 ⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∪ 𝐶))) | |
9 | dfss2 3886 | . 2 ⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐶)) | |
10 | 7, 8, 9 | 3bitr4i 306 | 1 ⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 847 ∀wal 1541 ∈ wcel 2110 ∖ cdif 3863 ∪ cun 3864 ⊆ wss 3866 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 |
This theorem is referenced by: difcom 4400 uneqdifeq 4404 ssunsn2 4740 elpwun 7554 soex 7699 ressuppssdif 7927 ssfi 8851 frfi 8916 cantnfp1lem3 9295 dfacfin7 10013 zornn0g 10119 fpwwe2lem12 10256 hashbclem 14016 incexclem 15400 ramub1lem1 16579 lpcls 22261 cmpcld 22299 alexsubALTlem3 22946 restmetu 23468 uniiccdif 24475 abelthlem2 25324 abelthlem3 25325 pmtrcnelor 31079 imadifss 35489 frege124d 41046 |
Copyright terms: Public domain | W3C validator |