Theorem 0un 4336

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 4098	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4334	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2759	1 ⊢ (∅ ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1542   ∪ cun 3887  ∅c0 4273

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274

This theorem is referenced by:  sspr  4778  sstp  4779  symdifv  5028  iunxdif3  5037  nlim2  8425  indconst0  12171  pwmndid  18907  pwmnd  18908  psdmullem  22131  ltslpss  27900  leslss  27901  mulsrid  28105  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  coprprop  32772  fzodif1  32865  cycpmrn  33204  bj-pr22val  37326  bj-snfromadj  37351  tfsconcat0i  43773  fiiuncl  45496  founiiun0  45620  infxrpnf  45874  prsal  46746  meadjun  46890  caragenuncllem  46940  carageniuncllem1  46949  hoidmvle  47028  iscnrm3rlem1  49415