Theorem 0un 4331

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 4095	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4329	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2763	1 ⊢ (∅ ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1547   ∪ cun 3888  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-un 3895  df-nul 4269

This theorem is referenced by:  sspr  4773  sstp  4774  symdifv  5022  iunxdif3  5031  nlim2  8422  indconst0  12169  pwmndid  18905  pwmnd  18906  psdmullem  22160  ltslpss  27925  leslss  27926  mulsrid  28130  mulsproplem5  28137  mulsproplem6  28138  mulsproplem7  28139  mulsproplem8  28140  coprprop  32798  fzodif1  32891  cycpmrn  33231  bj-pr22val  37379  bj-snfromadj  37404  tfsconcat0i  43797  fiiuncl  45520  founiiun0  45644  infxrpnf  45896  prsal  46768  meadjun  46912  caragenuncllem  46962  carageniuncllem1  46971  hoidmvle  47050  iscnrm3rlem1  49437