Theorem un0 4357

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 4299	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 952	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4118	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 860   = wceq 1567   ∈ wcel 2149   ∪ cun 3911  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-un 3918  df-nul 4295

This theorem is referenced by:  0un  4359  csbun  4404  un00  4408  disjssun  4431  difun2  4444  difdifdir  4454  disjpr2  4681  prprc1  4733  diftpsn3  4771  symdif0  5052  symdifid  5054  iununi  5066  unidif0  5328  unidif0OLD  5329  relresdm1  6033  difxp1  6161  difxp2  6162  suc0  6435  sucprc  6436  fresaun  6747  fresaunres2  6748  fvun1  6970  fndifnfp  7172  fvunsn  7175  fvsnun1  7178  fvsnun2  7179  fsnunfv  7183  fsnunres  7184  funiunfv  7244  fnsuppeq0  8184  frrlem12  8290  oev2  8504  oarec  8543  undifixp  8928  domss2  9120  unfi  9151  domunfican  9277  kmlem2  10131  kmlem3  10132  kmlem11  10140  dju0en  10155  djuassen  10158  ackbij1lem1  10198  ackbij1lem13  10210  fin1a2lem10  10389  fin1a2lem12  10391  axdc3lem4  10433  ttukeylem6  10494  alephadd  10558  fpwwe2lem12  10623  indconst1  12227  prunioo  13504  fzsuc2  13606  fseq1p1m1  13622  hashgval  14365  hashinf  14367  hashfun  14470  sadid1  16522  lcmfunsnlem  16695  lcmfun  16699  vdwap1  17033  setsres  17234  setsid  17263  mreexexlem3d  17698  mreexdomd  17701  pwmndid  18994  pwmnd  18995  pwssplit1  21154  lspsnat  21243  lsppratlem3  21247  opsrtoslem2  22172  indistopon  23123  indistps  23133  indistps2  23134  restcld  23294  neitr  23302  refun0  23637  filconn  24005  ufildr  24053  restmetu  24692  ovolioo  25692  itgsplitioo  25962  plyeq0  26333  birthdaylem2  27079  lgsquadlem2  27507  noextendseq  27793  nosupbnd2lem1  27841  noinfbnd2lem1  27856  noetasuplem2  27860  noetasuplem3  27861  noetasuplem4  27862  noetainflem2  27864  bday1  27969  lrold  28052  addsrid  28119  negsproplem2  28184  negsproplem6  28188  muls01  28267  mulsrid  28268  mulsproplem2  28272  mulsproplem3  28273  mulsproplem4  28274  mulsproplem12  28282  mulsproplem13  28283  mulsproplem14  28284  onleft  28415  ltonold  28416  oncutlt  28419  oniso  28426  bdayons  28431  onaddscl  28432  onmulscl  28433  n0cut  28489  n0bday  28507  bdayn0p1  28524  0reno  28651  1reno  28652  ex-dif  30711  ex-in  30713  ex-res  30729  difres  32882  imadifxp  32883  ofpreima2  32948  coprprop  32981  padct  33000  difico  33065  tocycf  33374  tocyc01  33375  elrgspnlem4  33502  esplyind  33906  constrextdg2lem  34079  locfinref  34172  sigaclfu2  34452  prsiga  34462  unelldsys  34489  measun  34542  difelcarsg  34641  carsgclctunlem1  34648  carsggect  34649  eulerpartlemt  34702  eulerpartgbij  34703  ballotlemfp1  34823  fineqvac  35448  indispconn  35621  onint1  36845  bj-pr21val  37533  bj-funun  37779  lindsdom  38148  poimirlem3  38157  poimirlem5  38159  poimirlem10  38164  poimirlem15  38169  poimirlem22  38176  poimirlem23  38177  poimirlem28  38182  padd01  40470  padd02  40471  pclfinclN  40609  mapfzcons1  43333  fzsplit1nn0  43370  diophrw  43375  eldioph2lem1  43376  eldioph2lem2  43377  diophren  43425  pwssplit4  43701  mnuprdlem1  44867  dvmptfprodlem  46543  caratheodorylem1  47125  isomenndlem  47129  fzopredsuc  47943  clnbgr0edg  48484  tposrescnv  49535  tposres2  49536  tposres3  49537  aacllem  50457