![]() |
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 4916. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unissi.1 | ⊢ 𝐴 ⊆ 𝐵 |
Ref | Expression |
---|---|
unissi | ⊢ ∪ 𝐴 ⊆ ∪ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unissi.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | uniss 4916 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 ⊆ ∪ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3948 ∪ cuni 4908 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3955 df-ss 3965 df-uni 4909 |
This theorem is referenced by: unidif 4946 unixpss 5810 riotassuni 7409 unifpw 9361 fiuni 9429 rankuni 9864 fin23lem29 10342 fin23lem30 10343 fin1a2lem12 10412 prdsds 17417 psss 18543 tgval2 22779 eltg4i 22783 ntrss2 22881 isopn3 22890 mretopd 22916 ordtbas 23016 cmpcov2 23214 tgcmp 23225 comppfsc 23356 alexsublem 23868 alexsubALTlem3 23873 alexsubALTlem4 23874 cldsubg 23935 bndth 24804 uniioombllem4 25435 uniioombllem5 25436 omssubadd 33764 cvmscld 34729 fnessref 35708 inunissunidif 36722 mblfinlem3 36993 mblfinlem4 36994 ismblfin 36995 mbfresfi 37000 cover2 37049 salexct 45511 salgencntex 45520 |
Copyright terms: Public domain | W3C validator |