| 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 34036 hashf2 34057 sxbrsigalem3 34246 signswch 34535 tz9.1regs 35073 bj-unrab 36910 bj-tagss 36964 bj-imdirco 37174 poimirlem16 37626 poimirlem19 37629 poimirlem23 37633 poimirlem29 37639 poimirlem31 37641 poimirlem32 37642 mblfinlem3 37649 mblfinlem4 37650 hdmapevec 41824 rtrclex 43600 trclexi 43603 rtrclexi 43604 cnvrcl0 43608 cnvtrcl0 43609 comptiunov2i 43689 cotrclrcl 43725 cncfiooicclem1 45884 fourierdlem62 46159 |
| Copyright terms: Public domain | W3C validator |