Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unssi | Structured version Visualization version GIF version |
Description: An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
unssi.1 | ⊢ 𝐴 ⊆ 𝐶 |
unssi.2 | ⊢ 𝐵 ⊆ 𝐶 |
Ref | Expression |
---|---|
unssi | ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unssi.1 | . . 3 ⊢ 𝐴 ⊆ 𝐶 | |
2 | unssi.2 | . . 3 ⊢ 𝐵 ⊆ 𝐶 | |
3 | 1, 2 | pm3.2i 471 | . 2 ⊢ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) |
4 | unss 3787 | . 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
5 | 3, 4 | mpbi 220 | 1 ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 384 ∪ cun 3572 ⊆ wss 3574 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-un 3579 df-in 3581 df-ss 3588 |
This theorem is referenced by: dmrnssfld 5384 tc2 8618 pwxpndom2 9487 ltrelxr 10099 nn0ssre 11296 nn0ssz 11398 dfle2 11980 difreicc 12304 hashxrcl 13148 ramxrcl 15721 strlemor1OLD 15969 strleun 15972 cssincl 20032 leordtval2 21016 lecldbas 21023 comppfsc 21335 aalioulem2 24088 taylfval 24113 axlowdimlem10 25831 shunssji 28228 shsval3i 28247 shjshsi 28351 spanuni 28403 sshhococi 28405 esumcst 30125 hashf2 30146 sxbrsigalem3 30334 signswch 30638 bj-unrab 32922 bj-tagss 32968 poimirlem16 33425 poimirlem19 33428 poimirlem23 33432 poimirlem29 33438 poimirlem31 33440 poimirlem32 33441 mblfinlem3 33448 mblfinlem4 33449 hdmapevec 37127 rtrclex 37924 trclexi 37927 rtrclexi 37928 cnvrcl0 37932 cnvtrcl0 37933 comptiunov2i 37998 cotrclrcl 38034 cncfiooicclem1 40106 fourierdlem62 40385 |
Copyright terms: Public domain | W3C validator |