Theorem 0un 4346

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

Assertion

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

Proof of Theorem 0un

Step	Hyp	Ref	Expression
1		uncom 4105	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4344	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2784	1 ⊢ (∅ ∪ 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3897  ∅c0 4279

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280

This theorem is used by:  sspr  4795  sstp  4796  symdifv  5046  iunxdif3  5055  nlim2  8482  indconst0  12313  pwmndid  19122  pwmnd  19123  psdmullem  22466  ltslpss  28276  leslss  28277  mulsrid  28481  mulsproplem5  28488  mulsproplem6  28489  mulsproplem7  28490  mulsproplem8  28491  coprprop  33274  fzodif1  33366  cycpmrn  33686  dflringlem3  34010  dflring4  34012  bj-pr22val  37902  bj-snfromadj  37927  tfsconcat0i  44305  fiiuncl  46025  founiiun0  46148  infxrpnf  46400  prsal  47272  meadjun  47416  caragenuncllem  47466  carageniuncllem1  47475  hoidmvle  47554  iscnrm3rlem1  49992