| 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 3968 | . 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶)) | |
| 2 | 19.26 1870 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) | |
| 3 | elunant 4184 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) | |
| 4 | 3 | albii 1819 | . . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
| 5 | df-ss 3968 | . . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
| 6 | df-ss 3968 | . . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) | |
| 7 | 5, 6 | anbi12i 628 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
| 8 | 2, 4, 7 | 3bitr4i 303 | . 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
| 9 | 1, 8 | bitr2i 276 | 1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 ∈ wcel 2108 ∪ cun 3949 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-ss 3968 |
| This theorem is referenced by: unssi 4191 unssd 4192 unssad 4193 unssbd 4194 nsspssun 4268 uneqin 4289 prssg 4819 ssunsn2 4827 tpss 4837 iunopeqop 5526 eqrelrel 5807 xpsspw 5819 relun 5821 relcoi2 6297 pwuncl 7790 fnsuppres 8216 wfrlem15OLD 8363 naddov3 8718 naddasslem1 8732 naddasslem2 8733 dfer2 8746 isinf 9296 isinfOLD 9297 trcl 9768 supxrun 13358 trclun 15053 isumltss 15884 rpnnen2lem12 16261 lcmfunsnlem 16678 lcmfun 16682 coprmprod 16698 coprmproddvdslem 16699 lubun 18560 isipodrs 18582 ipodrsima 18586 unocv 21698 aspval2 21918 uncld 23049 restntr 23190 cmpcld 23410 uncmp 23411 ufprim 23917 tsmsfbas 24136 ovolctb2 25527 ovolun 25534 unmbl 25572 plyun0 26236 noextendseq 27712 noresle 27742 madebdayim 27926 sshjcl 31374 sshjval2 31430 shlub 31433 ssjo 31466 spanuni 31563 cntzun 33071 unitprodclb 33417 dfon2lem3 35786 dfon2lem7 35790 clsun 36329 lindsadd 37620 lindsenlbs 37622 mblfinlem3 37666 ismblfin 37668 paddssat 39816 pclunN 39900 paddunN 39929 poldmj1N 39930 pclfinclN 39952 lsmfgcl 43086 tfsconcatrnss 43363 ssuncl 43583 sssymdifcl 43585 undmrnresiss 43617 mptrcllem 43626 cnvrcl0 43638 dfrtrcl5 43642 brtrclfv2 43740 unhe1 43798 dffrege76 43952 uneqsn 44038 mnurndlem1 44300 setrec1lem4 49209 elpglem2 49231 |
| Copyright terms: Public domain | W3C validator |