Theorem 0un 4356

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

Assertion

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

Proof of Theorem 0un

Step	Hyp	Ref	Expression
1		uncom 4115	. 2 ⊢ (∅ ∪ 𝐴) = (𝐴 ∪ ∅)
2		un0 4354	. 2 ⊢ (𝐴 ∪ ∅) = 𝐴
3	1, 2	eqtri 2789	1 ⊢ (∅ ∪ 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3906  ∅c0 4289

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-dif 3911  df-un 3913  df-nul 4290

This theorem is used by:  sspr  4805  sstp  4806  symdifv  5057  iunxdif3  5066  nlim2  8484  indconst0  12248  pwmndid  19029  pwmnd  19030  psdmullem  22365  ltslpss  28138  leslss  28139  mulsrid  28343  mulsproplem5  28350  mulsproplem6  28351  mulsproplem7  28352  mulsproplem8  28353  coprprop  33081  fzodif1  33174  cycpmrn  33494  dflringlem3  33817  dflring4  33819  bj-pr22val  37696  bj-snfromadj  37721  tfsconcat0i  44113  fiiuncl  45826  founiiun0  45949  infxrpnf  46201  prsal  47073  meadjun  47217  caragenuncllem  47267  carageniuncllem1  47276  hoidmvle  47355  iscnrm3rlem1  49759