![]() |
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 | df-ss 3963 | . 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶)) | |
2 | 19.26 1865 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) | |
3 | elunant 4178 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) | |
4 | 3 | albii 1813 | . . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
5 | df-ss 3963 | . . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
6 | df-ss 3963 | . . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) | |
7 | 5, 6 | anbi12i 626 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
8 | 2, 4, 7 | 3bitr4i 302 | . 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
9 | 1, 8 | bitr2i 275 | 1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∀wal 1531 ∈ wcel 2098 ∪ cun 3944 ⊆ wss 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-un 3951 df-ss 3963 |
This theorem is referenced by: unssi 4185 unssd 4186 unssad 4187 unssbd 4188 nsspssun 4258 uneqin 4279 prssg 4827 ssunsn2 4835 tpss 4843 iunopeqop 5526 eqrelrel 5802 xpsspw 5814 relun 5816 relcoi2 6287 pwuncl 7777 fnsuppres 8204 wfrlem15OLD 8352 naddov3 8709 naddasslem1 8723 naddasslem2 8724 dfer2 8734 isinf 9297 isinfOLD 9298 trcl 9767 supxrun 13344 trclun 15014 isumltss 15847 rpnnen2lem12 16222 lcmfunsnlem 16637 lcmfun 16641 coprmprod 16657 coprmproddvdslem 16658 lubun 18535 isipodrs 18557 ipodrsima 18561 unocv 21668 aspval2 21887 uncld 23028 restntr 23169 cmpcld 23389 uncmp 23390 ufprim 23896 tsmsfbas 24115 ovolctb2 25504 ovolun 25511 unmbl 25549 plyun0 26216 noextendseq 27689 noresle 27719 madebdayim 27903 sshjcl 31280 sshjval2 31336 shlub 31339 ssjo 31372 spanuni 31469 cntzun 32906 unitprodclb 33241 dfon2lem3 35557 dfon2lem7 35561 clsun 35988 lindsadd 37262 lindsenlbs 37264 mblfinlem3 37308 ismblfin 37310 paddssat 39461 pclunN 39545 paddunN 39574 poldmj1N 39575 pclfinclN 39597 lsmfgcl 42672 tfsconcatrnss 42953 ssuncl 43174 sssymdifcl 43176 undmrnresiss 43208 mptrcllem 43217 cnvrcl0 43229 dfrtrcl5 43233 brtrclfv2 43331 unhe1 43389 dffrege76 43543 uneqsn 43629 mnurndlem1 43892 setrec1lem4 48373 elpglem2 48395 |
Copyright terms: Public domain | W3C validator |