Theorem un0 4289

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 4232	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 936	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4058	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ∪ cun 3858  ∅c0 4227

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3863  df-un 3865  df-nul 4228

This theorem is referenced by:  0un  4291  csbun  4338  un00  4342  disjssun  4367  difun2  4380  difdifdir  4388  disjpr2  4609  prprc1  4661  diftpsn3  4695  sspr  4726  sstp  4727  symdif0  4975  symdifv  4976  symdifid  4977  iunxdif3  4985  iununi  4989  unidif0  5231  difxp1  5998  difxp2  5999  suc0  6247  sucprc  6248  fresaun  6538  fresaunres2  6539  fvssunirn  6691  fvun1  6747  fndifnfp  6934  fvunsn  6937  fvsnun1  6940  fvsnun2  6941  fsnunfv  6945  fsnunres  6946  funiunfv  7004  fnsuppeq0  7871  wfrlem14  7983  oev2  8163  oarec  8203  undifixp  8521  domss2  8703  unfi  8746  domunfican  8829  kmlem2  9616  kmlem3  9617  kmlem11  9625  dju0en  9640  djuassen  9643  ackbij1lem1  9685  ackbij1lem13  9697  fin1a2lem10  9874  fin1a2lem12  9876  axdc3lem4  9918  ttukeylem6  9979  alephadd  10042  fpwwe2lem12  10107  prunioo  12918  fzsuc2  13019  fseq1p1m1  13035  hashgval  13748  hashinf  13750  hashfun  13853  sadid1  15872  lcmfunsnlem  16042  lcmfun  16046  vdwap1  16373  setsres  16588  setsid  16601  mreexexlem3d  16980  mreexdomd  16983  pwmndid  18172  pwmnd  18173  pwssplit1  19904  lspsnat  19990  lsppratlem3  19994  opsrtoslem2  20821  indistopon  21706  indistps  21716  indistps2  21717  restcld  21877  neitr  21885  refun0  22220  filconn  22588  ufildr  22636  restmetu  23277  ovolioo  24273  itgsplitioo  24542  plyeq0  24912  birthdaylem2  25642  lgsquadlem2  26069  ex-dif  28312  ex-in  28314  ex-res  28330  difres  30466  imadifxp  30467  funresdm1  30471  ofpreima2  30531  coprprop  30560  padct  30582  difico  30632  tocycf  30914  tocyc01  30915  locfinref  31316  sigaclfu2  31612  prsiga  31622  unelldsys  31649  measun  31702  difelcarsg  31800  carsgclctunlem1  31807  carsggect  31808  eulerpartlemt  31861  eulerpartgbij  31862  ballotlemfp1  31981  indispconn  32716  frrlem12  33400  noextendseq  33459  nosupbnd2lem1  33507  noinfbnd2lem1  33522  noetasuplem2  33526  noetasuplem3  33527  noetasuplem4  33528  noetainflem2  33530  bday1s  33611  addsid1  33702  onint1  34213  bj-pr21val  34756  bj-funun  34973  lindsdom  35357  poimirlem3  35366  poimirlem5  35368  poimirlem10  35373  poimirlem15  35378  poimirlem22  35385  poimirlem23  35386  poimirlem28  35391  padd01  37413  padd02  37414  pclfinclN  37552  metakunt24  39696  mapfzcons1  40059  fzsplit1nn0  40096  diophrw  40101  eldioph2lem1  40102  eldioph2lem2  40103  diophren  40155  pwssplit4  40434  mnuprdlem1  41381  dvmptfprodlem  42980  caratheodorylem1  43559  isomenndlem  43563  fzopredsuc  44276  aacllem  45793