| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > unissi | Structured version Visualization version GIF version | ||
| Description: Subclass relationship for subclass union. Inference form of uniss 4915. (Contributed by David Moews, 1-May-2017.) |
| Ref | Expression |
|---|---|
| unissi.1 | ⊢ 𝐴 ⊆ 𝐵 |
| Ref | Expression |
|---|---|
| unissi | ⊢ ∪ 𝐴 ⊆ ∪ 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unissi.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
| 2 | uniss 4915 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 ⊆ ∪ 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: ⊆ wss 3951 ∪ cuni 4907 |
| 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-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-uni 4908 |
| This theorem is referenced by: unidif 4942 unixpss 5820 riotassuni 7428 unifpw 9395 fiuni 9468 rankuni 9903 fin23lem29 10381 fin23lem30 10382 fin1a2lem12 10451 prdsds 17509 psss 18625 tgval2 22963 eltg4i 22967 ntrss2 23065 isopn3 23074 mretopd 23100 ordtbas 23200 cmpcov2 23398 tgcmp 23409 comppfsc 23540 alexsublem 24052 alexsubALTlem3 24057 alexsubALTlem4 24058 cldsubg 24119 bndth 24990 uniioombllem4 25621 uniioombllem5 25622 omssubadd 34302 cvmscld 35278 fnessref 36358 inunissunidif 37376 mblfinlem3 37666 mblfinlem4 37667 ismblfin 37668 mbfresfi 37673 cover2 37722 salexct 46349 salgencntex 46358 |
| Copyright terms: Public domain | W3C validator |