![]() |
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 3930 | . 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
5 | 3, 4 | mpbi 220 | 1 ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 ∪ cun 3713 ⊆ wss 3715 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-un 3720 df-in 3722 df-ss 3729 |
This theorem is referenced by: dmrnssfld 5539 tc2 8793 pwxpndom2 9699 ltrelxr 10311 nn0ssre 11508 nn0ssz 11610 dfle2 12193 difreicc 12517 hashxrcl 13360 ramxrcl 15943 strlemor1OLD 16191 strleun 16194 cssincl 20254 leordtval2 21238 lecldbas 21245 comppfsc 21557 aalioulem2 24307 taylfval 24332 axlowdimlem10 26051 shunssji 28558 shsval3i 28577 shjshsi 28681 spanuni 28733 sshhococi 28735 esumcst 30455 hashf2 30476 sxbrsigalem3 30664 signswch 30968 bj-unrab 33247 bj-tagss 33292 poimirlem16 33756 poimirlem19 33759 poimirlem23 33763 poimirlem29 33769 poimirlem31 33771 poimirlem32 33772 mblfinlem3 33779 mblfinlem4 33780 hdmapevec 37647 rtrclex 38444 trclexi 38447 rtrclexi 38448 cnvrcl0 38452 cnvtrcl0 38453 comptiunov2i 38518 cotrclrcl 38554 cncfiooicclem1 40627 fourierdlem62 40906 |
Copyright terms: Public domain | W3C validator |