Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unss | Structured version Visualization version GIF version |
Description: The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.) |
Ref | Expression |
---|---|
unss | ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2 3557 | . 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶)) | |
2 | 19.26 1786 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) | |
3 | elun 3715 | . . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
4 | 3 | imbi1i 338 | . . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶)) |
5 | jaob 818 | . . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) | |
6 | 4, 5 | bitri 263 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
7 | 6 | albii 1737 | . . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
8 | dfss2 3557 | . . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
9 | dfss2 3557 | . . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) | |
10 | 8, 9 | anbi12i 729 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
11 | 2, 7, 10 | 3bitr4i 291 | . 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
12 | 1, 11 | bitr2i 264 | 1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∀wal 1473 ∈ wcel 1977 ∪ cun 3538 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-in 3547 df-ss 3554 |
This theorem is referenced by: unssi 3750 unssd 3751 unssad 3752 unssbd 3753 nsspssun 3819 uneqin 3837 uneqdifeqOLD 4010 prssg 4290 prssOLD 4292 ssunsn2 4299 tpss 4308 iunopeqop 4906 pwundif 4945 eqrelrel 5144 xpsspw 5156 relun 5158 relcoi2 5580 fnsuppres 7209 wfrlem15 7316 dfer2 7630 isinf 8058 fiin 8211 trcl 8487 supxrun 12018 trclun 13603 isumltss 14419 rpnnen2lem12 14793 lcmfunsnlem 15192 lcmfun 15196 coprmprod 15213 coprmproddvdslem 15214 lubun 16946 isipodrs 16984 fpwipodrs 16987 ipodrsima 16988 aspval2 19168 unocv 19843 uncld 20655 restntr 20796 cmpcld 21015 uncmp 21016 ufprim 21523 tsmsfbas 21741 ovolctb2 23067 ovolun 23074 unmbl 23112 plyun0 23757 sshjcl 27598 sshjval2 27654 shlub 27657 ssjo 27690 spanuni 27787 dfon2lem3 30934 dfon2lem7 30938 clsun 31493 lindsenlbs 32574 mblfinlem3 32618 ismblfin 32620 paddssat 34118 pclunN 34202 paddunN 34231 poldmj1N 34232 pclfinclN 34254 lsmfgcl 36662 ssuncl 36894 sssymdifcl 36896 undmrnresiss 36929 mptrcllem 36939 cnvrcl0 36951 dfrtrcl5 36955 brtrclfv2 37038 unhe1 37099 dffrege76 37253 uneqsn 37341 clsk1indlem3 37361 setrec1lem4 42236 elpglem2 42254 |
Copyright terms: Public domain | W3C validator |