Theorem un0 3810

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

Syntax hints:   \/ wo 368   = wceq 1379   e. wcel 1767   u. cun 3474   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-un 3481  df-nul 3786

This theorem is referenced by:  csbun  3857  un00  3862  disjssun  3884  difun2  3906  difdifdir  3914  disjpr2  4090  prprc1  4137  diftpsn3  4165  sspr  4190  sstp  4191  iununi  4410  unidif0  4620  suc0  4952  sucprc  4953  difxp1  5432  difxp2  5433  fresaun  5756  fresaunres2  5757  fvssunirn  5889  fvun1  5938  fmptpr  6086  fndifnfp  6090  fvunsn  6093  fvsnun1  6096  fvsnun2  6097  fsnunfv  6101  fsnunres  6102  fnsuppeq0OLD  6122  funiunfv  6148  fnsuppeq0  6928  oev2  7173  oarec  7211  undifixp  7505  domss2  7676  domunfican  7793  kmlem2  8531  kmlem3  8532  kmlem11  8540  cda0en  8559  cdaassen  8562  ackbij1lem1  8600  ackbij1lem13  8612  fin1a2lem10  8789  fin1a2lem12  8791  axdc3lem4  8833  ttukeylem6  8894  alephadd  8952  fpwwe2lem13  9020  prunioo  11649  fzsuc2  11737  fseq1p1m1  11752  hashgval  12376  hashinf  12378  hashfun  12461  sadid1  13977  vdwap1  14354  setsres  14518  setsid  14531  mreexexlem3d  14901  mreexdomd  14904  pwssplit1  17505  lspsnat  17591  lsppratlem3  17595  opsrtoslem2  17948  indistopon  19296  indistps  19306  indistps2  19307  restcld  19467  neitr  19475  filcon  20147  ufildr  20195  restmetu  20853  ovolioo  21741  itgsplitioo  22007  plyeq0  22371  birthdaylem2  23038  lgsquadlem2  23386  constr3pthlem1  24359  ex-dif  24849  ex-in  24851  ex-res  24867  difres  27158  imadifxp  27159  ofpreima2  27208  difico  27290  sigaclfu2  27789  prsiga  27799  measun  27850  eulerpartlemt  27978  eulerpartgbij  27979  ballotlemfp1  28098  indispcon  28347  wfrlem14  28961  nofulllem1  29067  nofulllem2  29068  symdif0  29079  symdifV  29080  symdifid  29081  onint1  29519  mapfzcons1  30281  fzsplit1nn0  30319  diophrw  30324  eldioph2lem1  30325  eldioph2lem2  30326  diophren  30379  pwssplit4  30667  bj-pr21val  33670  bj-pr22val  33676  padd01  34625  padd02  34626  pclfinclN  34764