| 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 470 | . 2 ⊢ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) |
| 4 | unss 4190 | . 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
| 5 | 3, 4 | mpbi 230 | 1 ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 ∪ 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: pwunss 4618 dmrnssfld 5984 tc2 9782 djuunxp 9961 pwxpndom2 10705 ltrelxr 11322 nn0ssre 12530 nn0sscn 12531 nn0ssz 12636 dfle2 13189 difreicc 13524 hashxrcl 14396 ramxrcl 17055 strleun 17194 cssincl 21706 leordtval2 23220 lecldbas 23227 comppfsc 23540 aalioulem2 26375 taylfval 26400 addsbdaylem 28049 addsbday 28050 addsdilem3 28179 addsdilem4 28180 mulsasslem3 28191 pw2bday 28418 axlowdimlem10 28966 shunssji 31388 shsval3i 31407 shjshsi 31511 spanuni 31563 sshhococi 31565 esumcst 34064 hashf2 34085 sxbrsigalem3 34274 signswch 34576 bj-unrab 36927 bj-tagss 36981 bj-imdirco 37191 poimirlem16 37643 poimirlem19 37646 poimirlem23 37650 poimirlem29 37656 poimirlem31 37658 poimirlem32 37659 mblfinlem3 37666 mblfinlem4 37667 hdmapevec 41837 rtrclex 43630 trclexi 43633 rtrclexi 43634 cnvrcl0 43638 cnvtrcl0 43639 comptiunov2i 43719 cotrclrcl 43755 cncfiooicclem1 45908 fourierdlem62 46183 |
| Copyright terms: Public domain | W3C validator |