Theorem 0un 4345

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 4107	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4343	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2756	1 ⊢ (∅ ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1541   ∪ cun 3896  ∅c0 4282

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-un 3903  df-nul 4283

This theorem is referenced by:  nlim2  8411  pwmndid  18846  pwmnd  18847  psdmullem  22081  sltlpss  27854  slelss  27855  mulsrid  28053  mulsproplem5  28060  mulsproplem6  28061  mulsproplem7  28062  mulsproplem8  28063  coprprop  32684  fzodif1  32779  indconst0  32846  cycpmrn  33119  bj-pr22val  37084  bj-snfromadj  37109  tfsconcat0i  43462  fiiuncl  45186  founiiun0  45311  infxrpnf  45568  prsal  46440  meadjun  46584  caragenuncllem  46634  carageniuncllem1  46643  hoidmvle  46722  iscnrm3rlem1  49064