Theorem un0 4321

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 4261	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 935	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 223	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4081	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 843   = wceq 1539   ∈ wcel 2108   ∪ cun 3881  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254

This theorem is referenced by:  0un  4323  csbun  4369  un00  4373  disjssun  4398  difun2  4411  difdifdir  4419  disjpr2  4646  prprc1  4698  diftpsn3  4732  sspr  4763  sstp  4764  symdif0  5010  symdifv  5011  symdifid  5012  iunxdif3  5020  iununi  5024  unidif0  5277  difxp1  6057  difxp2  6058  suc0  6325  sucprc  6326  fresaun  6629  fresaunres2  6630  fvssunirn  6785  fvun1  6841  fndifnfp  7030  fvunsn  7033  fvsnun1  7036  fvsnun2  7037  fsnunfv  7041  fsnunres  7042  funiunfv  7103  fnsuppeq0  7979  frrlem12  8084  wfrlem14OLD  8124  oev2  8315  oarec  8355  undifixp  8680  domss2  8872  unfi  8917  domunfican  9017  kmlem2  9838  kmlem3  9839  kmlem11  9847  dju0en  9862  djuassen  9865  ackbij1lem1  9907  ackbij1lem13  9919  fin1a2lem10  10096  fin1a2lem12  10098  axdc3lem4  10140  ttukeylem6  10201  alephadd  10264  fpwwe2lem12  10329  prunioo  13142  fzsuc2  13243  fseq1p1m1  13259  hashgval  13975  hashinf  13977  hashfun  14080  sadid1  16103  lcmfunsnlem  16274  lcmfun  16278  vdwap1  16606  setsres  16807  setsid  16837  mreexexlem3d  17272  mreexdomd  17275  pwmndid  18490  pwmnd  18491  pwssplit1  20236  lspsnat  20322  lsppratlem3  20326  opsrtoslem2  21173  indistopon  22059  indistps  22069  indistps2  22070  restcld  22231  neitr  22239  refun0  22574  filconn  22942  ufildr  22990  restmetu  23632  ovolioo  24637  itgsplitioo  24907  plyeq0  25277  birthdaylem2  26007  lgsquadlem2  26434  ex-dif  28688  ex-in  28690  ex-res  28706  difres  30840  imadifxp  30841  funresdm1  30845  ofpreima2  30905  coprprop  30934  padct  30956  difico  31006  tocycf  31286  tocyc01  31287  locfinref  31693  sigaclfu2  31989  prsiga  31999  unelldsys  32026  measun  32079  difelcarsg  32177  carsgclctunlem1  32184  carsggect  32185  eulerpartlemt  32238  eulerpartgbij  32239  ballotlemfp1  32358  fineqvac  32966  indispconn  33096  noextendseq  33797  nosupbnd2lem1  33845  noinfbnd2lem1  33860  noetasuplem2  33864  noetasuplem3  33865  noetasuplem4  33866  noetainflem2  33868  bday1s  33952  lrold  34004  addsid1  34054  onint1  34565  bj-pr21val  35130  bj-funun  35350  lindsdom  35698  poimirlem3  35707  poimirlem5  35709  poimirlem10  35714  poimirlem15  35719  poimirlem22  35726  poimirlem23  35727  poimirlem28  35732  padd01  37752  padd02  37753  pclfinclN  37891  metakunt24  40076  mapfzcons1  40455  fzsplit1nn0  40492  diophrw  40497  eldioph2lem1  40498  eldioph2lem2  40499  diophren  40551  pwssplit4  40830  mnuprdlem1  41779  dvmptfprodlem  43375  caratheodorylem1  43954  isomenndlem  43958  fzopredsuc  44703  aacllem  46391