Theorem un0 4346

Description: The union of a class with the empty set is itself. 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 4290	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 939	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 224	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4108	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ∪ cun 3899  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286

This theorem is referenced by:  0un  4348  csbun  4393  un00  4397  disjssun  4420  difun2  4433  difdifdir  4444  disjpr2  4670  prprc1  4722  diftpsn3  4758  sspr  4791  sstp  4792  symdif0  5040  symdifv  5041  symdifid  5042  iunxdif3  5050  iununi  5054  unidif0  5305  relresdm1  5992  difxp1  6123  difxp2  6124  suc0  6394  sucprc  6395  fresaun  6705  fresaunres2  6706  fvun1  6925  fndifnfp  7122  fvunsn  7125  fvsnun1  7128  fvsnun2  7129  fsnunfv  7133  fsnunres  7134  funiunfv  7194  fnsuppeq0  8134  frrlem12  8239  oev2  8450  oarec  8489  undifixp  8872  domss2  9064  unfi  9095  domunfican  9222  kmlem2  10062  kmlem3  10063  kmlem11  10071  dju0en  10086  djuassen  10089  ackbij1lem1  10129  ackbij1lem13  10141  fin1a2lem10  10319  fin1a2lem12  10321  axdc3lem4  10363  ttukeylem6  10424  alephadd  10488  fpwwe2lem12  10553  prunioo  13397  fzsuc2  13498  fseq1p1m1  13514  hashgval  14256  hashinf  14258  hashfun  14360  sadid1  16395  lcmfunsnlem  16568  lcmfun  16572  vdwap1  16905  setsres  17105  setsid  17134  mreexexlem3d  17569  mreexdomd  17572  pwmndid  18861  pwmnd  18862  pwssplit1  21011  lspsnat  21100  lsppratlem3  21104  opsrtoslem2  22011  indistopon  22945  indistps  22955  indistps2  22956  restcld  23116  neitr  23124  refun0  23459  filconn  23827  ufildr  23875  restmetu  24514  ovolioo  25525  itgsplitioo  25795  plyeq0  26172  birthdaylem2  26918  lgsquadlem2  27348  noextendseq  27635  nosupbnd2lem1  27683  noinfbnd2lem1  27698  noetasuplem2  27702  noetasuplem3  27703  noetasuplem4  27704  noetainflem2  27706  bday1  27810  lrold  27893  addsrid  27960  negsproplem2  28025  negsproplem6  28029  muls01  28108  mulsrid  28109  mulsproplem2  28113  mulsproplem3  28114  mulsproplem4  28115  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  onleft  28256  ltonold  28257  oncutlt  28260  oniso  28267  bdayons  28272  onaddscl  28273  onmulscl  28274  n0cut  28330  n0bday  28348  bdayn0p1  28365  0reno  28492  1reno  28493  ex-dif  30498  ex-in  30500  ex-res  30516  difres  32675  imadifxp  32676  ofpreima2  32744  coprprop  32778  padct  32797  difico  32863  indconst1  32940  tocycf  33199  tocyc01  33200  elrgspnlem4  33327  esplyind  33731  constrextdg2lem  33905  locfinref  33998  sigaclfu2  34278  prsiga  34288  unelldsys  34315  measun  34368  difelcarsg  34467  carsgclctunlem1  34474  carsggect  34475  eulerpartlemt  34528  eulerpartgbij  34529  ballotlemfp1  34649  fineqvac  35272  indispconn  35428  onint1  36643  bj-pr21val  37214  bj-funun  37453  lindsdom  37811  poimirlem3  37820  poimirlem5  37822  poimirlem10  37827  poimirlem15  37832  poimirlem22  37839  poimirlem23  37840  poimirlem28  37845  padd01  40067  padd02  40068  pclfinclN  40206  mapfzcons1  42955  fzsplit1nn0  42992  diophrw  42997  eldioph2lem1  42998  eldioph2lem2  42999  diophren  43051  pwssplit4  43327  mnuprdlem1  44509  dvmptfprodlem  46184  caratheodorylem1  46766  isomenndlem  46770  fzopredsuc  47565  clnbgr0edg  48079  tposrescnv  49120  tposres2  49121  tposres3  49122  aacllem  50042