Theorem un0 4417

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

Syntax hints:   ∨ wo 846   = wceq 1537   ∈ wcel 2108   ∪ cun 3974  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353

This theorem is referenced by:  0un  4419  csbun  4464  un00  4468  disjssun  4491  difun2  4504  difdifdir  4515  disjpr2  4738  prprc1  4790  diftpsn3  4827  sspr  4860  sstp  4861  symdif0  5108  symdifv  5109  symdifid  5110  iunxdif3  5118  iununi  5122  unidif0  5378  relresdm1  6062  difxp1  6196  difxp2  6197  suc0  6470  sucprc  6471  fresaun  6792  fresaunres2  6793  fvssunirnOLD  6954  fvun1  7013  fndifnfp  7210  fvunsn  7213  fvsnun1  7216  fvsnun2  7217  fsnunfv  7221  fsnunres  7222  funiunfv  7285  fnsuppeq0  8233  frrlem12  8338  wfrlem14OLD  8378  oev2  8579  oarec  8618  undifixp  8992  domss2  9202  unfi  9238  domunfican  9389  kmlem2  10221  kmlem3  10222  kmlem11  10230  dju0en  10245  djuassen  10248  ackbij1lem1  10288  ackbij1lem13  10300  fin1a2lem10  10478  fin1a2lem12  10480  axdc3lem4  10522  ttukeylem6  10583  alephadd  10646  fpwwe2lem12  10711  prunioo  13541  fzsuc2  13642  fseq1p1m1  13658  hashgval  14382  hashinf  14384  hashfun  14486  sadid1  16514  lcmfunsnlem  16688  lcmfun  16692  vdwap1  17024  setsres  17225  setsid  17255  mreexexlem3d  17704  mreexdomd  17707  pwmndid  18971  pwmnd  18972  pwssplit1  21081  lspsnat  21170  lsppratlem3  21174  opsrtoslem2  22103  indistopon  23029  indistps  23039  indistps2  23040  restcld  23201  neitr  23209  refun0  23544  filconn  23912  ufildr  23960  restmetu  24604  ovolioo  25622  itgsplitioo  25893  plyeq0  26270  birthdaylem2  27013  lgsquadlem2  27443  noextendseq  27730  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetasuplem2  27797  noetasuplem3  27798  noetasuplem4  27799  noetainflem2  27801  bday1s  27894  lrold  27953  addsrid  28015  negsproplem2  28079  negsproplem6  28083  muls01  28156  mulsrid  28157  mulsproplem2  28161  mulsproplem3  28162  mulsproplem4  28163  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  sltonold  28301  onaddscl  28304  onmulscl  28305  n0scut  28356  n0sbday  28372  ex-dif  30455  ex-in  30457  ex-res  30473  difres  32622  imadifxp  32623  ofpreima2  32684  coprprop  32711  padct  32733  difico  32788  tocycf  33110  tocyc01  33111  locfinref  33787  sigaclfu2  34085  prsiga  34095  unelldsys  34122  measun  34175  difelcarsg  34275  carsgclctunlem1  34282  carsggect  34283  eulerpartlemt  34336  eulerpartgbij  34337  ballotlemfp1  34456  fineqvac  35073  indispconn  35202  onint1  36415  bj-pr21val  36979  bj-funun  37218  lindsdom  37574  poimirlem3  37583  poimirlem5  37585  poimirlem10  37590  poimirlem15  37595  poimirlem22  37602  poimirlem23  37603  poimirlem28  37608  padd01  39768  padd02  39769  pclfinclN  39907  metakunt24  42185  mapfzcons1  42673  fzsplit1nn0  42710  diophrw  42715  eldioph2lem1  42716  eldioph2lem2  42717  diophren  42769  pwssplit4  43046  mnuprdlem1  44241  dvmptfprodlem  45865  caratheodorylem1  46447  isomenndlem  46451  fzopredsuc  47238  clnbgr0edg  47709  aacllem  48895