Theorem un0 3796

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 3774	. . . 4 |- -. x e. (/)
2	1	biorfi 407	. . 3 |- ( x e. A <-> ( x e. A \/ x e. (/) ) )
3	2	bicomi 202	. 2 |- ( ( x e. A \/ x e. (/) ) <-> x e. A )
4	3	uneqri 3631	1 |- ( A u. (/) ) = A

Syntax hints:   \/ wo 368   = wceq 1383   e. wcel 1804   u. cun 3459   (/)c0 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464  df-un 3466  df-nul 3771

This theorem is referenced by:  csbun  3843  un00  3848  disjssun  3870  difun2  3893  difdifdir  3901  disjpr2  4077  prprc1  4125  diftpsn3  4153  sspr  4178  sstp  4179  iununi  4400  unidif0  4610  suc0  4942  sucprc  4943  difxp1  5422  difxp2  5423  fresaun  5746  fresaunres2  5747  fvssunirn  5879  fvun1  5929  fndifnfp  6085  fvunsn  6088  fvsnun1  6091  fvsnun2  6092  fsnunfv  6096  fsnunres  6097  fnsuppeq0OLD  6117  funiunfv  6145  fnsuppeq0  6930  oev2  7175  oarec  7213  undifixp  7507  domss2  7678  domunfican  7795  kmlem2  8534  kmlem3  8535  kmlem11  8543  cda0en  8562  cdaassen  8565  ackbij1lem1  8603  ackbij1lem13  8615  fin1a2lem10  8792  fin1a2lem12  8794  axdc3lem4  8836  ttukeylem6  8897  alephadd  8955  fpwwe2lem13  9023  prunioo  11660  fzsuc2  11748  fseq1p1m1  11763  hashgval  12390  hashinf  12392  hashfun  12477  sadid1  14100  vdwap1  14477  setsres  14642  setsid  14655  mreexexlem3d  15025  mreexdomd  15028  pwssplit1  17684  lspsnat  17770  lsppratlem3  17774  opsrtoslem2  18128  indistopon  19480  indistps  19490  indistps2  19491  restcld  19651  neitr  19659  refun0  19994  filcon  20362  ufildr  20410  restmetu  21068  ovolioo  21956  itgsplitioo  22222  plyeq0  22586  birthdaylem2  23260  lgsquadlem2  23608  constr3pthlem1  24633  ex-dif  25122  ex-in  25124  ex-res  25140  difres  27435  imadifxp  27436  ofpreima2  27486  difico  27572  locfinref  27822  sigaclfu2  28099  prsiga  28109  measun  28160  eulerpartlemt  28288  eulerpartgbij  28289  ballotlemfp1  28408  indispcon  28657  wfrlem14  29332  nofulllem1  29438  nofulllem2  29439  symdif0  29450  symdifV  29451  symdifid  29452  onint1  29890  mapfzcons1  30625  fzsplit1nn0  30663  diophrw  30668  eldioph2lem1  30669  eldioph2lem2  30670  diophren  30723  pwssplit4  31011  dvmptfprodlem  31695  bj-pr21val  34454  bj-pr22val  34460  padd01  35410  padd02  35411  pclfinclN  35549