Theorem 0un 4354

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

Assertion

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

Proof of Theorem 0un

Step	Hyp	Ref	Expression
1		uncom 4113	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4352	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2786	1 ⊢ (∅ ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1570   ∪ cun 3904  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-un 3911  df-nul 4288

This theorem is referenced by:  sspr  4801  sstp  4802  symdifv  5053  iunxdif3  5062  nlim2  8476  indconst0  12231  pwmndid  18999  pwmnd  19000  psdmullem  22309  ltslpss  28079  leslss  28080  mulsrid  28284  mulsproplem5  28291  mulsproplem6  28292  mulsproplem7  28293  mulsproplem8  28294  coprprop  33022  fzodif1  33115  cycpmrn  33441  dflringlem3  33764  dflring4  33766  bj-pr22val  37633  bj-snfromadj  37658  tfsconcat0i  44052  fiiuncl  45765  founiiun0  45888  infxrpnf  46140  prsal  47012  meadjun  47156  caragenuncllem  47206  carageniuncllem1  47215  hoidmvle  47294  iscnrm3rlem1  49695