![]() |
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 4681. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unissi.1 | ⊢ 𝐴 ⊆ 𝐵 |
Ref | Expression |
---|---|
unissi | ⊢ ∪ 𝐴 ⊆ ∪ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unissi.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | uniss 4681 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 ⊆ ∪ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3798 ∪ cuni 4658 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-in 3805 df-ss 3812 df-uni 4659 |
This theorem is referenced by: unidif 4693 unixpss 5468 riotassuni 6903 unifpw 8538 fiuni 8603 rankuni 9003 fin23lem29 9478 fin23lem30 9479 fin1a2lem12 9548 prdsds 16477 psss 17567 tgval2 21131 eltg4i 21135 ntrss2 21232 isopn3 21241 mretopd 21267 ordtbas 21367 cmpcov2 21564 tgcmp 21575 comppfsc 21706 alexsublem 22218 alexsubALTlem3 22223 alexsubALTlem4 22224 cldsubg 22284 bndth 23127 uniioombllem4 23752 uniioombllem5 23753 omssubadd 30907 cvmscld 31801 fnessref 32890 mblfinlem3 33992 mblfinlem4 33993 ismblfin 33994 mbfresfi 33999 cover2 34051 salexct 41343 salgencntex 41352 |
Copyright terms: Public domain | W3C validator |