Theorem un0 3661

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

Syntax hints:   \/ wo 368   = wceq 1369   e. wcel 1756   u. cun 3325   (/)c0 3636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2973  df-dif 3330  df-un 3332  df-nul 3637

This theorem is referenced by:  csbun  3708  un00  3713  disjssun  3735  difun2  3757  difdifdir  3765  disjpr2  3937  prprc1  3984  diftpsn3  4011  sspr  4035  sstp  4036  iununi  4254  unidif0  4464  suc0  4792  sucprc  4793  difxp1  5262  difxp2  5263  fresaun  5581  fresaunres2  5582  fvssunirn  5712  fvun1  5761  fmptpr  5902  fndifnfp  5906  fvunsn  5909  fvsnun1  5912  fvsnun2  5913  fsnunfv  5917  fsnunres  5918  fnsuppeq0OLD  5938  funiunfv  5964  fnsuppeq0  6716  oev2  6962  oarec  7000  undifixp  7298  domss2  7469  domunfican  7583  kmlem2  8319  kmlem3  8320  kmlem11  8328  cda0en  8347  cdaassen  8350  ackbij1lem1  8388  ackbij1lem13  8400  fin1a2lem10  8577  fin1a2lem12  8579  axdc3lem4  8621  ttukeylem6  8682  alephadd  8740  fpwwe2lem13  8808  prunioo  11413  fzsuc2  11513  fseq1p1m1  11533  hashgval  12105  hashinf  12107  hashfun  12198  sadid1  13663  vdwap1  14037  setsres  14201  setsid  14214  mreexexlem3d  14583  mreexdomd  14586  pwssplit1  17139  lspsnat  17225  lsppratlem3  17229  opsrtoslem2  17565  indistopon  18604  indistps  18614  indistps2  18615  restcld  18775  neitr  18783  filcon  19455  ufildr  19503  restmetu  20161  ovolioo  21048  itgsplitioo  21314  plyeq0  21678  birthdaylem2  22345  lgsquadlem2  22693  constr3pthlem1  23540  ex-dif  23629  ex-in  23631  ex-res  23647  imadifxp  25938  ofpreima2  25984  difico  26072  sigaclfu2  26563  prsiga  26573  measun  26624  eulerpartlemt  26753  eulerpartgbij  26754  ballotlemfp1  26873  indispcon  27122  wfrlem14  27736  nofulllem1  27842  nofulllem2  27843  symdif0  27854  symdifV  27855  symdifid  27856  onint1  28294  mapfzcons1  29051  fzsplit1nn0  29090  diophrw  29095  eldioph2lem1  29096  eldioph2lem2  29097  diophren  29150  pwssplit4  29440  bj-pr21val  32504  bj-pr22val  32510  padd01  33453  padd02  33454  pclfinclN  33592