Theorem 0un 4348

Description: The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Assertion

Ref	Expression
0un	⊢ (∅ ∪ 𝐴) = 𝐴

Proof of Theorem 0un

Step	Hyp	Ref	Expression
1		uncom 4110	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4346	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2759	1 ⊢ (∅ ∪ 𝐴) = 𝐴

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