Theorem 0un 4350

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 4112	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4348	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2760	1 ⊢ (∅ ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1542   ∪ cun 3901  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-un 3908  df-nul 4288

This theorem is referenced by:  nlim2  8427  pwmndid  18873  pwmnd  18874  psdmullem  22120  ltslpss  27916  leslss  27917  mulsrid  28121  mulsproplem5  28128  mulsproplem6  28129  mulsproplem7  28130  mulsproplem8  28131  coprprop  32788  fzodif1  32882  indconst0  32949  cycpmrn  33236  bj-pr22val  37261  bj-snfromadj  37286  tfsconcat0i  43696  fiiuncl  45419  founiiun0  45543  infxrpnf  45798  prsal  46670  meadjun  46814  caragenuncllem  46864  carageniuncllem1  46873  hoidmvle  46952  iscnrm3rlem1  49293