Theorem un0 4347

Description: The union of a class with the empty set is itself. Dual of inv1 4351. Commuted form of 0un 4349. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
un0	⊢ (𝐴 ∪ ∅) = 𝐴

Proof of Theorem un0

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4287	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 953	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4106	1 ⊢ (𝐴 ∪ ∅) = 𝐴

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ∪ 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:  0un  4349  un00  4360  csbun  4402  disjssun  4424  difun2  4440  difdifdir  4450  disjpr2  4677  prprc1  4729  diftpsn3  4768  symdif0  5049  symdifid  5051  iununi  5063  unidif0  5328  unidif0OLD  5329  relresdm1  6033  difxp1  6161  difxp2  6162  suc0  6439  sucprc  6440  fresaun  6750  fresaunres2  6751  fvun1  6973  fndifnfp  7178  fvunsn  7181  fvsnun1  7184  fvsnun2  7185  fsnunfv  7189  fsnunres  7190  funiunfv  7249  fnsuppeq0  8194  frrlem12  8300  oev2  8514  oarec  8553  undifixp  8945  domss2  9138  unfi  9169  domunfican  9295  kmlem2  10158  kmlem3  10159  kmlem11  10167  dju0en  10182  djuassen  10185  ackbij1lem1  10225  ackbij1lem13  10237  fin1a2lem10  10415  fin1a2lem12  10417  axdc3lem4  10459  ttukeylem6  10520  alephadd  10590  fpwwe2lem12  10655  indconst1  12259  prunioo  13538  fzsuc2  13641  fseq1p1m1  13657  hashgval  14401  hashinf  14403  hashfun  14506  sadid1  16564  lcmfunsnlem  16737  lcmfun  16741  vdwap1  17075  setsres  17276  setsid  17305  mreexexlem3d  17740  mreexdomd  17743  pwmndid  19061  pwmnd  19062  pwssplit1  21249  lspsnat  21338  lsppratlem3  21342  lindsdom  22069  opsrtoslem2  22278  indistopon  23232  indistps  23242  indistps2  23243  restcld  23403  neitr  23411  refun0  23747  filconn  24115  ufildr  24163  restmetu  24802  ovolioo  25802  itgsplitioo  26072  plyeq0  26444  birthdaylem2  27197  lgsquadlem2  27625  noextendseq  27911  nosupbnd2lem1  27959  noinfbnd2lem1  27974  noetasuplem2  27978  noetasuplem3  27979  noetasuplem4  27980  noetainflem2  27982  bday1  28087  lrold  28170  addsrid  28237  negsproplem2  28302  negsproplem6  28306  muls01  28385  mulsrid  28386  mulsproplem2  28390  mulsproplem3  28391  mulsproplem4  28392  mulsproplem12  28400  mulsproplem13  28401  mulsproplem14  28402  onleft  28533  ltonold  28534  oncutlt  28537  oniso  28544  bdayons  28549  onaddscl  28550  onmulscl  28551  n0cut  28607  n0bday  28625  bdayn0p1  28642  0reno  28769  1reno  28770  ex-dif  30911  ex-in  30913  ex-res  30929  difres  33081  imadifxp  33082  ofpreima2  33147  coprprop  33179  padct  33197  difico  33262  tocycf  33565  tocyc01  33566  elrgspnlem4  33693  esplyind  34093  constrextdg2lem  34266  locfinref  34359  sigaclfu2  34639  prsiga  34649  unelldsys  34677  measun  34730  difelcarsg  34829  carsgclctunlem1  34836  carsggect  34837  eulerpartlemt  34890  eulerpartgbij  34891  ballotlemfp1  35011  fineqvac  35650  indispconn  35821  onint1  37076  bj-pr21val  37765  bj-funun  38012  poimirlem3  38380  poimirlem5  38382  poimirlem10  38387  poimirlem15  38392  poimirlem22  38399  poimirlem23  38400  poimirlem28  38405  padd01  40692  padd02  40693  pclfinclN  40831  mapfzcons1  43570  fzsplit1nn0  43607  diophrw  43612  eldioph2lem1  43613  eldioph2lem2  43614  diophren  43662  pwssplit4  43938  mnuprdlem1  45104  dvmptfprodlem  46780  caratheodorylem1  47362  isomenndlem  47366  fzopredsuc  48220  clnbgr0edg  48761  tposrescnv  49813  tposres2  49814  tposres3  49815  aacllem  50780