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 4157 | . 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
5 | 3, 4 | mpbi 231 | 1 ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 ∪ cun 3931 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-un 3938 df-in 3940 df-ss 3949 |
This theorem is referenced by: pwunss 5446 dmrnssfld 5834 tc2 9172 djuunxp 9338 pwxpndom2 10075 ltrelxr 10690 nn0ssre 11889 nn0sscn 11890 nn0ssz 11991 dfle2 12528 difreicc 12858 hashxrcl 13706 ramxrcl 16341 strleun 16579 cssincl 20760 leordtval2 21748 lecldbas 21755 comppfsc 22068 aalioulem2 24849 taylfval 24874 axlowdimlem10 26664 shunssji 29073 shsval3i 29092 shjshsi 29196 spanuni 29248 sshhococi 29250 esumcst 31221 hashf2 31242 sxbrsigalem3 31429 signswch 31730 bj-unrab 34141 bj-tagss 34189 poimirlem16 34789 poimirlem19 34792 poimirlem23 34796 poimirlem29 34802 poimirlem31 34804 poimirlem32 34805 mblfinlem3 34812 mblfinlem4 34813 hdmapevec 38851 rtrclex 39855 trclexi 39858 rtrclexi 39859 cnvrcl0 39863 cnvtrcl0 39864 comptiunov2i 39929 cotrclrcl 39965 cncfiooicclem1 42052 fourierdlem62 42330 |
Copyright terms: Public domain | W3C validator |