Theorem un0 4399

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

Syntax hints:   ∨ wo 847   = wceq 1536   ∈ wcel 2105   ∪ cun 3960  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967  df-nul 4339

This theorem is referenced by:  0un  4401  csbun  4446  un00  4450  disjssun  4473  difun2  4486  difdifdir  4497  disjpr2  4717  prprc1  4769  diftpsn3  4806  sspr  4839  sstp  4840  symdif0  5089  symdifv  5090  symdifid  5091  iunxdif3  5099  iununi  5103  unidif0  5365  relresdm1  6052  difxp1  6186  difxp2  6187  suc0  6460  sucprc  6461  fresaun  6779  fresaunres2  6780  fvssunirnOLD  6940  fvun1  6999  fndifnfp  7195  fvunsn  7198  fvsnun1  7201  fvsnun2  7202  fsnunfv  7206  fsnunres  7207  funiunfv  7267  fnsuppeq0  8215  frrlem12  8320  wfrlem14OLD  8360  oev2  8559  oarec  8598  undifixp  8972  domss2  9174  unfi  9209  domunfican  9358  kmlem2  10189  kmlem3  10190  kmlem11  10198  dju0en  10213  djuassen  10216  ackbij1lem1  10256  ackbij1lem13  10268  fin1a2lem10  10446  fin1a2lem12  10448  axdc3lem4  10490  ttukeylem6  10551  alephadd  10614  fpwwe2lem12  10679  prunioo  13517  fzsuc2  13618  fseq1p1m1  13634  hashgval  14368  hashinf  14370  hashfun  14472  sadid1  16501  lcmfunsnlem  16674  lcmfun  16678  vdwap1  17010  setsres  17211  setsid  17241  mreexexlem3d  17690  mreexdomd  17693  pwmndid  18961  pwmnd  18962  pwssplit1  21075  lspsnat  21164  lsppratlem3  21168  opsrtoslem2  22097  indistopon  23023  indistps  23033  indistps2  23034  restcld  23195  neitr  23203  refun0  23538  filconn  23906  ufildr  23954  restmetu  24598  ovolioo  25616  itgsplitioo  25887  plyeq0  26264  birthdaylem2  27009  lgsquadlem2  27439  noextendseq  27726  nosupbnd2lem1  27774  noinfbnd2lem1  27789  noetasuplem2  27793  noetasuplem3  27794  noetasuplem4  27795  noetainflem2  27797  bday1s  27890  lrold  27949  addsrid  28011  negsproplem2  28075  negsproplem6  28079  muls01  28152  mulsrid  28153  mulsproplem2  28157  mulsproplem3  28158  mulsproplem4  28159  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  sltonold  28297  onaddscl  28300  onmulscl  28301  n0scut  28352  n0sbday  28368  ex-dif  30451  ex-in  30453  ex-res  30469  difres  32619  imadifxp  32620  ofpreima2  32682  coprprop  32713  padct  32736  difico  32791  tocycf  33119  tocyc01  33120  elrgspnlem4  33234  locfinref  33801  sigaclfu2  34101  prsiga  34111  unelldsys  34138  measun  34191  difelcarsg  34291  carsgclctunlem1  34298  carsggect  34299  eulerpartlemt  34352  eulerpartgbij  34353  ballotlemfp1  34472  fineqvac  35089  indispconn  35218  onint1  36431  bj-pr21val  36995  bj-funun  37234  lindsdom  37600  poimirlem3  37609  poimirlem5  37611  poimirlem10  37616  poimirlem15  37621  poimirlem22  37628  poimirlem23  37629  poimirlem28  37634  padd01  39793  padd02  39794  pclfinclN  39932  metakunt24  42209  mapfzcons1  42704  fzsplit1nn0  42741  diophrw  42746  eldioph2lem1  42747  eldioph2lem2  42748  diophren  42800  pwssplit4  43077  mnuprdlem1  44267  dvmptfprodlem  45899  caratheodorylem1  46481  isomenndlem  46485  fzopredsuc  47272  clnbgr0edg  47760  aacllem  49031