Theorem un0 4334

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

Syntax hints:   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3887  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274

This theorem is referenced by:  0un  4336  csbun  4381  un00  4385  disjssun  4408  difun2  4421  difdifdir  4431  disjpr2  4657  prprc1  4709  diftpsn3  4747  symdif0  5027  symdifid  5029  iununi  5041  unidif0  5301  unidif0OLD  5302  relresdm1  5998  difxp1  6129  difxp2  6130  suc0  6400  sucprc  6401  fresaun  6711  fresaunres2  6712  fvun1  6931  fndifnfp  7131  fvunsn  7134  fvsnun1  7137  fvsnun2  7138  fsnunfv  7142  fsnunres  7143  funiunfv  7203  fnsuppeq0  8142  frrlem12  8247  oev2  8458  oarec  8497  undifixp  8882  domss2  9074  unfi  9105  domunfican  9232  kmlem2  10074  kmlem3  10075  kmlem11  10083  dju0en  10098  djuassen  10101  ackbij1lem1  10141  ackbij1lem13  10153  fin1a2lem10  10331  fin1a2lem12  10333  axdc3lem4  10375  ttukeylem6  10436  alephadd  10500  fpwwe2lem12  10565  indconst1  12172  prunioo  13434  fzsuc2  13536  fseq1p1m1  13552  hashgval  14295  hashinf  14297  hashfun  14399  sadid1  16437  lcmfunsnlem  16610  lcmfun  16614  vdwap1  16948  setsres  17148  setsid  17177  mreexexlem3d  17612  mreexdomd  17615  pwmndid  18907  pwmnd  18908  pwssplit1  21054  lspsnat  21143  lsppratlem3  21147  opsrtoslem2  22034  indistopon  22966  indistps  22976  indistps2  22977  restcld  23137  neitr  23145  refun0  23480  filconn  23848  ufildr  23896  restmetu  24535  ovolioo  25535  itgsplitioo  25805  plyeq0  26176  birthdaylem2  26916  lgsquadlem2  27344  noextendseq  27631  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem2  27698  noetasuplem3  27699  noetasuplem4  27700  noetainflem2  27702  bday1  27806  lrold  27889  addsrid  27956  negsproplem2  28021  negsproplem6  28025  muls01  28104  mulsrid  28105  mulsproplem2  28109  mulsproplem3  28110  mulsproplem4  28111  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  onleft  28252  ltonold  28253  oncutlt  28256  oniso  28263  bdayons  28268  onaddscl  28269  onmulscl  28270  n0cut  28326  n0bday  28344  bdayn0p1  28361  0reno  28488  1reno  28489  ex-dif  30493  ex-in  30495  ex-res  30511  difres  32670  imadifxp  32671  ofpreima2  32739  coprprop  32772  padct  32791  difico  32856  tocycf  33178  tocyc01  33179  elrgspnlem4  33306  esplyind  33719  constrextdg2lem  33892  locfinref  33985  sigaclfu2  34265  prsiga  34275  unelldsys  34302  measun  34355  difelcarsg  34454  carsgclctunlem1  34461  carsggect  34462  eulerpartlemt  34515  eulerpartgbij  34516  ballotlemfp1  34636  fineqvac  35260  indispconn  35416  onint1  36631  bj-pr21val  37320  bj-funun  37566  lindsdom  37935  poimirlem3  37944  poimirlem5  37946  poimirlem10  37951  poimirlem15  37956  poimirlem22  37963  poimirlem23  37964  poimirlem28  37969  padd01  40257  padd02  40258  pclfinclN  40396  mapfzcons1  43149  fzsplit1nn0  43186  diophrw  43191  eldioph2lem1  43192  eldioph2lem2  43193  diophren  43241  pwssplit4  43517  mnuprdlem1  44699  dvmptfprodlem  46372  caratheodorylem1  46954  isomenndlem  46958  fzopredsuc  47772  clnbgr0edg  48313  tposrescnv  49354  tposres2  49355  tposres3  49356  aacllem  50276