Theorem 0un 4337

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

Syntax hints:   = wceq 1542   ∪ cun 3888  ∅c0 4274

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 3432  df-dif 3893  df-un 3895  df-nul 4275

This theorem is referenced by:  sspr  4779  sstp  4780  symdifv  5029  iunxdif3  5038  nlim2  8418  indconst0  12162  pwmndid  18898  pwmnd  18899  psdmullem  22141  ltslpss  27914  leslss  27915  mulsrid  28119  mulsproplem5  28126  mulsproplem6  28127  mulsproplem7  28128  mulsproplem8  28129  coprprop  32787  fzodif1  32880  cycpmrn  33219  bj-pr22val  37342  bj-snfromadj  37367  tfsconcat0i  43791  fiiuncl  45514  founiiun0  45638  infxrpnf  45892  prsal  46764  meadjun  46908  caragenuncllem  46958  carageniuncllem1  46967  hoidmvle  47046  iscnrm3rlem1  49427