| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 0un | Structured version Visualization version GIF version | ||
| Description: The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| Ref | Expression |
|---|---|
| 0un | ⊢ (∅ ∪ 𝐴) = 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uncom 4110 | . 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅) | |
| 2 | un0 4346 | . 2 ⊢ (𝐴 ∪ ∅) = 𝐴 | |
| 3 | 1, 2 | eqtri 2759 | 1 ⊢ (∅ ∪ 𝐴) = 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1541 ∪ cun 3899 ∅c0 4285 |
| 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 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-v 3442 df-dif 3904 df-un 3906 df-nul 4286 |
| This theorem is referenced by: nlim2 8417 pwmndid 18861 pwmnd 18862 psdmullem 22108 ltslpss 27904 leslss 27905 mulsrid 28109 mulsproplem5 28116 mulsproplem6 28117 mulsproplem7 28118 mulsproplem8 28119 coprprop 32778 fzodif1 32872 indconst0 32939 cycpmrn 33225 bj-pr22val 37220 bj-snfromadj 37245 tfsconcat0i 43583 fiiuncl 45306 founiiun0 45430 infxrpnf 45686 prsal 46558 meadjun 46702 caragenuncllem 46752 carageniuncllem1 46761 hoidmvle 46840 iscnrm3rlem1 49181 |
| Copyright terms: Public domain | W3C validator |