Theorem un0 4343

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-un 3903  df-nul 4283

This theorem is referenced by:  0un  4345  csbun  4390  un00  4394  disjssun  4417  difun2  4430  difdifdir  4441  disjpr2  4665  prprc1  4717  diftpsn3  4753  sspr  4786  sstp  4787  symdif0  5035  symdifv  5036  symdifid  5037  iunxdif3  5045  iununi  5049  unidif0  5300  relresdm1  5986  difxp1  6117  difxp2  6118  suc0  6388  sucprc  6389  fresaun  6699  fresaunres2  6700  fvun1  6919  fndifnfp  7116  fvunsn  7119  fvsnun1  7122  fvsnun2  7123  fsnunfv  7127  fsnunres  7128  funiunfv  7188  fnsuppeq0  8128  frrlem12  8233  oev2  8444  oarec  8483  undifixp  8864  domss2  9056  unfi  9087  domunfican  9213  kmlem2  10050  kmlem3  10051  kmlem11  10059  dju0en  10074  djuassen  10077  ackbij1lem1  10117  ackbij1lem13  10129  fin1a2lem10  10307  fin1a2lem12  10309  axdc3lem4  10351  ttukeylem6  10412  alephadd  10475  fpwwe2lem12  10540  prunioo  13383  fzsuc2  13484  fseq1p1m1  13500  hashgval  14242  hashinf  14244  hashfun  14346  sadid1  16381  lcmfunsnlem  16554  lcmfun  16558  vdwap1  16891  setsres  17091  setsid  17120  mreexexlem3d  17554  mreexdomd  17557  pwmndid  18846  pwmnd  18847  pwssplit1  20995  lspsnat  21084  lsppratlem3  21088  opsrtoslem2  21992  indistopon  22917  indistps  22927  indistps2  22928  restcld  23088  neitr  23096  refun0  23431  filconn  23799  ufildr  23847  restmetu  24486  ovolioo  25497  itgsplitioo  25767  plyeq0  26144  birthdaylem2  26890  lgsquadlem2  27320  noextendseq  27607  nosupbnd2lem1  27655  noinfbnd2lem1  27670  noetasuplem2  27674  noetasuplem3  27675  noetasuplem4  27676  noetainflem2  27678  bday1s  27776  lrold  27843  addsrid  27908  negsproplem2  27972  negsproplem6  27976  muls01  28052  mulsrid  28053  mulsproplem2  28057  mulsproplem3  28058  mulsproplem4  28059  mulsproplem12  28067  mulsproplem13  28068  mulsproplem14  28069  onsleft  28198  sltonold  28199  onscutlt  28202  onsiso  28206  bdayon  28210  onaddscl  28211  onmulscl  28212  n0scut  28263  n0sbday  28281  bdayn0p1  28295  ex-dif  30405  ex-in  30407  ex-res  30423  difres  32582  imadifxp  32583  ofpreima2  32650  coprprop  32684  padct  32705  difico  32770  indconst1  32847  tocycf  33093  tocyc01  33094  elrgspnlem4  33219  esplyind  33613  constrextdg2lem  33782  locfinref  33875  sigaclfu2  34155  prsiga  34165  unelldsys  34192  measun  34245  difelcarsg  34344  carsgclctunlem1  34351  carsggect  34352  eulerpartlemt  34405  eulerpartgbij  34406  ballotlemfp1  34526  fineqvac  35160  indispconn  35299  onint1  36514  bj-pr21val  37078  bj-funun  37317  lindsdom  37675  poimirlem3  37684  poimirlem5  37686  poimirlem10  37691  poimirlem15  37696  poimirlem22  37703  poimirlem23  37704  poimirlem28  37709  padd01  39931  padd02  39932  pclfinclN  40070  mapfzcons1  42835  fzsplit1nn0  42872  diophrw  42877  eldioph2lem1  42878  eldioph2lem2  42879  diophren  42931  pwssplit4  43207  mnuprdlem1  44390  dvmptfprodlem  46067  caratheodorylem1  46649  isomenndlem  46653  fzopredsuc  47448  clnbgr0edg  47962  tposrescnv  49004  tposres2  49005  tposres3  49006  aacllem  49927