Theorem un0 3759

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	|- ( A u. (/) ) = A

Proof of Theorem un0

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3735	. . . 4 |- -. x e. (/)
2	1	biorfi 409	. . 3 |- ( x e. A <-> ( x e. A \/ x e. (/) ) )
3	2	bicomi 206	. 2 |- ( ( x e. A \/ x e. (/) ) <-> x e. A )
4	3	uneqri 3576	1 |- ( A u. (/) ) = A

Syntax hints:   \/ wo 370   = wceq 1444   e. wcel 1887   u. cun 3402   (/)c0 3731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-dif 3407  df-un 3409  df-nul 3732

This theorem is referenced by:  csbun  3798  un00  3800  disjssun  3822  difun2  3847  difdifdir  3855  disjpr2  4034  prprc1  4082  diftpsn3  4110  sspr  4135  sstp  4136  symdif0  4355  symdifv  4356  symdifid  4357  iununi  4366  unidif0  4576  difxp1  5262  difxp2  5263  suc0  5497  sucprc  5498  fresaun  5754  fresaunres2  5755  fvssunirn  5888  fvun1  5936  fndifnfp  6093  fvunsn  6096  fvsnun1  6099  fvsnun2  6100  fsnunfv  6104  fsnunres  6105  funiunfv  6153  fnsuppeq0  6943  wfrlem14  7049  oev2  7225  oarec  7263  undifixp  7558  domss2  7731  domunfican  7844  kmlem2  8581  kmlem3  8582  kmlem11  8590  cda0en  8609  cdaassen  8612  ackbij1lem1  8650  ackbij1lem13  8662  fin1a2lem10  8839  fin1a2lem12  8841  axdc3lem4  8883  ttukeylem6  8944  alephadd  9002  fpwwe2lem13  9067  prunioo  11761  fzsuc2  11853  fseq1p1m1  11868  hashgval  12518  hashinf  12520  hashfun  12609  sadid1  14442  lcmfunsnlem  14614  lcmfun  14618  vdwap1  14927  setsres  15151  setsid  15164  mreexexlem3d  15552  mreexdomd  15555  pwssplit1  18282  lspsnat  18368  lsppratlem3  18372  opsrtoslem2  18708  indistopon  20016  indistps  20026  indistps2  20027  restcld  20188  neitr  20196  refun0  20530  filcon  20898  ufildr  20946  restmetu  21585  ovolioo  22521  itgsplitioo  22795  plyeq0  23165  birthdaylem2  23878  lgsquadlem2  24283  constr3pthlem1  25383  ex-dif  25873  ex-in  25875  ex-res  25891  iunxdif3  28175  difres  28211  imadifxp  28212  ofpreima2  28269  padct  28307  difico  28365  locfinref  28668  sigaclfu2  28943  prsiga  28953  unelldsys  28980  measun  29033  difelcarsg  29142  carsgclctunlem1  29149  carsggect  29150  eulerpartlemt  29204  eulerpartgbij  29205  ballotlemfp1  29324  indispcon  29957  nofulllem1  30591  nofulllem2  30592  onint1  31109  bj-pr21val  31607  bj-pr22val  31613  poimirlem3  31943  poimirlem5  31945  poimirlem10  31950  poimirlem15  31955  poimirlem22  31962  poimirlem23  31963  poimirlem28  31968  padd01  33376  padd02  33377  pclfinclN  33515  mapfzcons1  35559  fzsplit1nn0  35596  diophrw  35601  eldioph2lem1  35602  eldioph2lem2  35603  diophren  35656  pwssplit4  35947  0un  37386  dvmptfprodlem  37819  prsal  38179  caratheodorylem1  38347  isomenndlem  38351  fzopredsuc  38720  aacllem  40593