| 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 4141 | . 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
| 5 | 3, 4 | mpbi 230 | 1 ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 ∪ cun 3901 ⊆ wss 3903 |
| 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 2008 ax-8 2111 ax-9 2119 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1543 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-v 3438 df-un 3908 df-ss 3920 |
| This theorem is referenced by: pwunss 4569 dmrnssfld 5915 tc2 9638 djuunxp 9817 pwxpndom2 10559 ltrelxr 11176 nn0ssre 12388 nn0sscn 12389 nn0ssz 12494 dfle2 13049 difreicc 13387 hashxrcl 14264 ramxrcl 16929 strleun 17068 cssincl 21595 leordtval2 23097 lecldbas 23104 comppfsc 23417 aalioulem2 26239 taylfval 26264 addsbdaylem 27928 addsbday 27929 addsdilem3 28061 addsdilem4 28062 mulsasslem3 28073 onscutlt 28170 axlowdimlem10 28896 shunssji 31313 shsval3i 31332 shjshsi 31436 spanuni 31488 sshhococi 31490 esumcst 34030 hashf2 34051 sxbrsigalem3 34240 signswch 34529 tz9.1regs 35067 bj-unrab 36904 bj-tagss 36958 bj-imdirco 37168 poimirlem16 37620 poimirlem19 37623 poimirlem23 37627 poimirlem29 37633 poimirlem31 37635 poimirlem32 37636 mblfinlem3 37643 mblfinlem4 37644 hdmapevec 41818 rtrclex 43594 trclexi 43597 rtrclexi 43598 cnvrcl0 43602 cnvtrcl0 43603 comptiunov2i 43683 cotrclrcl 43719 cncfiooicclem1 45878 fourierdlem62 46153 |
| Copyright terms: Public domain | W3C validator |