![]() |
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 3624 | . 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶)) | |
2 | 19.26 1838 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) | |
3 | elun 3786 | . . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
4 | 3 | imbi1i 338 | . . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶)) |
5 | jaob 839 | . . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) | |
6 | 4, 5 | bitri 264 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
7 | 6 | albii 1787 | . . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
8 | dfss2 3624 | . . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
9 | dfss2 3624 | . . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) | |
10 | 8, 9 | anbi12i 733 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
11 | 2, 7, 10 | 3bitr4i 292 | . 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
12 | 1, 11 | bitr2i 265 | 1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∨ wo 382 ∧ wa 383 ∀wal 1521 ∈ wcel 2030 ∪ cun 3605 ⊆ wss 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-un 3612 df-in 3614 df-ss 3621 |
This theorem is referenced by: unssi 3821 unssd 3822 unssad 3823 unssbd 3824 nsspssun 3890 uneqin 3911 uneqdifeqOLD 4091 prssg 4382 prssOLD 4384 ssunsn2 4391 tpss 4400 iunopeqop 5010 pwundif 5050 eqrelrel 5255 xpsspw 5266 relun 5268 relcoi2 5701 fnsuppres 7367 wfrlem15 7474 dfer2 7788 isinf 8214 fiin 8369 trcl 8642 supxrun 12184 trclun 13799 isumltss 14624 rpnnen2lem12 14998 lcmfunsnlem 15401 lcmfun 15405 coprmprod 15422 coprmproddvdslem 15423 lubun 17170 isipodrs 17208 fpwipodrs 17211 ipodrsima 17212 aspval2 19395 unocv 20072 uncld 20893 restntr 21034 cmpcld 21253 uncmp 21254 ufprim 21760 tsmsfbas 21978 ovolctb2 23306 ovolun 23313 unmbl 23351 plyun0 23998 sshjcl 28342 sshjval2 28398 shlub 28401 ssjo 28434 spanuni 28531 dfon2lem3 31814 dfon2lem7 31818 noextendseq 31945 noresle 31971 clsun 32448 lindsenlbs 33534 mblfinlem3 33578 ismblfin 33580 paddssat 35418 pclunN 35502 paddunN 35531 poldmj1N 35532 pclfinclN 35554 lsmfgcl 37961 ssuncl 38192 sssymdifcl 38194 undmrnresiss 38227 mptrcllem 38237 cnvrcl0 38249 dfrtrcl5 38253 brtrclfv2 38336 unhe1 38396 dffrege76 38550 uneqsn 38638 clsk1indlem3 38658 setrec1lem4 42762 elpglem2 42783 |
Copyright terms: Public domain | W3C validator |