Theorem 0un 4345

Description: The union of the empty set with a class is itself. Commuted form of un0 4343. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Assertion

Ref	Expression
0un	⊢ (∅ ∪ 𝐴) = 𝐴

Proof of Theorem 0un

Step	Hyp	Ref	Expression
1		uncom 4157	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4343	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2783	1 ⊢ (∅ ∪ 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4149  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047  df-un 4151  df-nul 4279

This theorem is used by:  sspr  4789  sstp  4790  symdifv  5045  iunxdif3  5054  nlim2  8501  indconst0  12335  pwmndid  19147  pwmnd  19148  psdmullem  22491  ltslpss  28299  leslss  28300  mulsrid  28504  mulsproplem5  28511  mulsproplem6  28512  mulsproplem7  28513  mulsproplem8  28514  coprprop  33339  fzodif1  33430  cycpmrn  33750  dflringlem3  34074  dflring4  34076  j00smo  35944  maxssj0  35945  bj-pr22val  38024  bj-snfromadj  38049  tfsconcat0i  44440  fiiuncl  46175  founiiun0  46298  infxrpnf  46549  prsal  47421  meadjun  47565  caragenuncllem  47615  carageniuncllem1  47624  hoidmvle  47703  iscnrm3rlem1  50147