Theorem 0un 4349

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

Assertion

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

Proof of Theorem 0un

Step	Hyp	Ref	Expression
1		uncom 4108	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4347	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2785	1 ⊢ (∅ ∪ 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3900  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905  df-un 3907  df-nul 4283

This theorem is used by:  sspr  4798  sstp  4799  symdifv  5050  iunxdif3  5059  nlim2  8481  indconst0  12258  pwmndid  19061  pwmnd  19062  psdmullem  22399  ltslpss  28181  leslss  28182  mulsrid  28386  mulsproplem5  28393  mulsproplem6  28394  mulsproplem7  28395  mulsproplem8  28396  coprprop  33179  fzodif1  33271  cycpmrn  33591  dflringlem3  33914  dflring4  33916  bj-pr22val  37771  bj-snfromadj  37796  tfsconcat0i  44194  fiiuncl  45907  founiiun0  46030  infxrpnf  46282  prsal  47154  meadjun  47298  caragenuncllem  47348  carageniuncllem1  47357  hoidmvle  47436  iscnrm3rlem1  49874