Theorem un0 3650

Description: The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-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 3629	. . . 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 3486	1 |- ( A u. (/) ) = A

Syntax hints:   \/ wo 368   = wceq 1362   e. wcel 1755   u. cun 3314   (/)c0 3625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319  df-un 3321  df-nul 3626

This theorem is referenced by:  csbun  3697  un00  3702  disjssun  3724  difun2  3746  difdifdir  3754  disjpr2  3926  prprc1  3973  diftpsn3  4000  sspr  4024  sstp  4025  iununi  4243  unidif0  4453  suc0  4780  sucprc  4781  difxp1  5251  difxp2  5252  fresaun  5570  fresaunres2  5571  fvssunirn  5701  fvun1  5750  fmptpr  5890  fndifnfp  5894  fvunsn  5897  fvsnun1  5900  fvsnun2  5901  fsnunfv  5905  fsnunres  5906  fnsuppeq0OLD  5926  funiunfv  5952  fnsuppeq0  6706  oev2  6951  oarec  6989  undifixp  7287  domss2  7458  domunfican  7572  kmlem2  8308  kmlem3  8309  kmlem11  8317  cda0en  8336  cdaassen  8339  ackbij1lem1  8377  ackbij1lem13  8389  fin1a2lem10  8566  fin1a2lem12  8568  axdc3lem4  8610  ttukeylem6  8671  alephadd  8729  fpwwe2lem13  8796  prunioo  11400  fzsuc2  11498  fseq1p1m1  11517  hashgval  12089  hashinf  12091  hashfun  12182  sadid1  13646  vdwap1  14020  setsres  14184  setsid  14197  mreexexlem3d  14566  mreexdomd  14569  pwssplit1  17061  lspsnat  17147  lsppratlem3  17151  opsrtoslem2  17497  indistopon  18446  indistps  18456  indistps2  18457  restcld  18617  neitr  18625  filcon  19297  ufildr  19345  restmetu  20003  ovolioo  20890  itgsplitioo  21156  plyeq0  21563  birthdaylem2  22230  lgsquadlem2  22578  constr3pthlem1  23363  ex-dif  23452  ex-in  23454  ex-res  23470  imadifxp  25762  ofpreima2  25808  difico  25895  sigaclfu2  26417  prsiga  26427  measun  26478  eulerpartlemt  26601  eulerpartgbij  26602  ballotlemfp1  26721  indispcon  26970  wfrlem14  27583  nofulllem1  27689  nofulllem2  27690  symdif0  27701  symdifV  27702  symdifid  27703  onint1  28142  mapfzcons1  28895  fzsplit1nn0  28934  diophrw  28939  eldioph2lem1  28940  eldioph2lem2  28941  diophren  28994  pwssplit4  29284  bj-pr21val  32086  bj-pr22val  32092  padd01  33025  padd02  33026  pclfinclN  33164