Theorem un0 4369

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

Syntax hints:   ∨ wo 847   = wceq 1540   ∈ wcel 2108   ∪ cun 3924  ∅c0 4308

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-nul 4309

This theorem is referenced by:  0un  4371  csbun  4416  un00  4420  disjssun  4443  difun2  4456  difdifdir  4467  disjpr2  4689  prprc1  4741  diftpsn3  4778  sspr  4811  sstp  4812  symdif0  5061  symdifv  5062  symdifid  5063  iunxdif3  5071  iununi  5075  unidif0  5330  relresdm1  6020  difxp1  6154  difxp2  6155  suc0  6428  sucprc  6429  fresaun  6748  fresaunres2  6749  fvssunirnOLD  6909  fvun1  6969  fndifnfp  7167  fvunsn  7170  fvsnun1  7173  fvsnun2  7174  fsnunfv  7178  fsnunres  7179  funiunfv  7239  fnsuppeq0  8189  frrlem12  8294  wfrlem14OLD  8334  oev2  8533  oarec  8572  undifixp  8946  domss2  9148  unfi  9183  domunfican  9331  kmlem2  10164  kmlem3  10165  kmlem11  10173  dju0en  10188  djuassen  10191  ackbij1lem1  10231  ackbij1lem13  10243  fin1a2lem10  10421  fin1a2lem12  10423  axdc3lem4  10465  ttukeylem6  10526  alephadd  10589  fpwwe2lem12  10654  prunioo  13496  fzsuc2  13597  fseq1p1m1  13613  hashgval  14349  hashinf  14351  hashfun  14453  sadid1  16485  lcmfunsnlem  16658  lcmfun  16662  vdwap1  16995  setsres  17195  setsid  17224  mreexexlem3d  17656  mreexdomd  17659  pwmndid  18912  pwmnd  18913  pwssplit1  21015  lspsnat  21104  lsppratlem3  21108  opsrtoslem2  22012  indistopon  22937  indistps  22947  indistps2  22948  restcld  23108  neitr  23116  refun0  23451  filconn  23819  ufildr  23867  restmetu  24507  ovolioo  25519  itgsplitioo  25789  plyeq0  26166  birthdaylem2  26912  lgsquadlem2  27342  noextendseq  27629  nosupbnd2lem1  27677  noinfbnd2lem1  27692  noetasuplem2  27696  noetasuplem3  27697  noetasuplem4  27698  noetainflem2  27700  bday1s  27793  lrold  27852  addsrid  27914  negsproplem2  27978  negsproplem6  27982  muls01  28055  mulsrid  28056  mulsproplem2  28060  mulsproplem3  28061  mulsproplem4  28062  mulsproplem12  28070  mulsproplem13  28071  mulsproplem14  28072  sltonold  28200  onaddscl  28203  onmulscl  28204  n0scut  28255  n0sbday  28271  ex-dif  30350  ex-in  30352  ex-res  30368  difres  32527  imadifxp  32528  ofpreima2  32590  coprprop  32622  padct  32643  difico  32706  tocycf  33074  tocyc01  33075  elrgspnlem4  33186  constrextdg2lem  33728  locfinref  33818  sigaclfu2  34098  prsiga  34108  unelldsys  34135  measun  34188  difelcarsg  34288  carsgclctunlem1  34295  carsggect  34296  eulerpartlemt  34349  eulerpartgbij  34350  ballotlemfp1  34470  fineqvac  35074  indispconn  35202  onint1  36413  bj-pr21val  36977  bj-funun  37216  lindsdom  37584  poimirlem3  37593  poimirlem5  37595  poimirlem10  37600  poimirlem15  37605  poimirlem22  37612  poimirlem23  37613  poimirlem28  37618  padd01  39776  padd02  39777  pclfinclN  39915  metakunt24  42187  mapfzcons1  42687  fzsplit1nn0  42724  diophrw  42729  eldioph2lem1  42730  eldioph2lem2  42731  diophren  42783  pwssplit4  43060  mnuprdlem1  44244  dvmptfprodlem  45921  caratheodorylem1  46503  isomenndlem  46507  fzopredsuc  47300  clnbgr0edg  47798  tposrescnv  48802  tposres2  48803  tposres3  48804  aacllem  49613