Theorem un0 4394

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 4338	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 940	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 224	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4156	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 848   = wceq 1540   ∈ wcel 2108   ∪ cun 3949  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334

This theorem is referenced by:  0un  4396  csbun  4441  un00  4445  disjssun  4468  difun2  4481  difdifdir  4492  disjpr2  4713  prprc1  4765  diftpsn3  4802  sspr  4835  sstp  4836  symdif0  5085  symdifv  5086  symdifid  5087  iunxdif3  5095  iununi  5099  unidif0  5360  relresdm1  6051  difxp1  6185  difxp2  6186  suc0  6459  sucprc  6460  fresaun  6779  fresaunres2  6780  fvssunirnOLD  6940  fvun1  7000  fndifnfp  7196  fvunsn  7199  fvsnun1  7202  fvsnun2  7203  fsnunfv  7207  fsnunres  7208  funiunfv  7268  fnsuppeq0  8217  frrlem12  8322  wfrlem14OLD  8362  oev2  8561  oarec  8600  undifixp  8974  domss2  9176  unfi  9211  domunfican  9361  kmlem2  10192  kmlem3  10193  kmlem11  10201  dju0en  10216  djuassen  10219  ackbij1lem1  10259  ackbij1lem13  10271  fin1a2lem10  10449  fin1a2lem12  10451  axdc3lem4  10493  ttukeylem6  10554  alephadd  10617  fpwwe2lem12  10682  prunioo  13521  fzsuc2  13622  fseq1p1m1  13638  hashgval  14372  hashinf  14374  hashfun  14476  sadid1  16505  lcmfunsnlem  16678  lcmfun  16682  vdwap1  17015  setsres  17215  setsid  17244  mreexexlem3d  17689  mreexdomd  17692  pwmndid  18949  pwmnd  18950  pwssplit1  21058  lspsnat  21147  lsppratlem3  21151  opsrtoslem2  22080  indistopon  23008  indistps  23018  indistps2  23019  restcld  23180  neitr  23188  refun0  23523  filconn  23891  ufildr  23939  restmetu  24583  ovolioo  25603  itgsplitioo  25873  plyeq0  26250  birthdaylem2  26995  lgsquadlem2  27425  noextendseq  27712  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem2  27779  noetasuplem3  27780  noetasuplem4  27781  noetainflem2  27783  bday1s  27876  lrold  27935  addsrid  27997  negsproplem2  28061  negsproplem6  28065  muls01  28138  mulsrid  28139  mulsproplem2  28143  mulsproplem3  28144  mulsproplem4  28145  mulsproplem12  28153  mulsproplem13  28154  mulsproplem14  28155  sltonold  28283  onaddscl  28286  onmulscl  28287  n0scut  28338  n0sbday  28354  ex-dif  30442  ex-in  30444  ex-res  30460  difres  32613  imadifxp  32614  ofpreima2  32676  coprprop  32708  padct  32731  difico  32785  tocycf  33137  tocyc01  33138  elrgspnlem4  33249  constrextdg2lem  33789  locfinref  33840  sigaclfu2  34122  prsiga  34132  unelldsys  34159  measun  34212  difelcarsg  34312  carsgclctunlem1  34319  carsggect  34320  eulerpartlemt  34373  eulerpartgbij  34374  ballotlemfp1  34494  fineqvac  35111  indispconn  35239  onint1  36450  bj-pr21val  37014  bj-funun  37253  lindsdom  37621  poimirlem3  37630  poimirlem5  37632  poimirlem10  37637  poimirlem15  37642  poimirlem22  37649  poimirlem23  37650  poimirlem28  37655  padd01  39813  padd02  39814  pclfinclN  39952  metakunt24  42229  mapfzcons1  42728  fzsplit1nn0  42765  diophrw  42770  eldioph2lem1  42771  eldioph2lem2  42772  diophren  42824  pwssplit4  43101  mnuprdlem1  44291  dvmptfprodlem  45959  caratheodorylem1  46541  isomenndlem  46545  fzopredsuc  47335  clnbgr0edg  47823  tposrescnv  48779  tposres2  48780  tposres3  48781  aacllem  49320