Theorem un0 3784

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 3762	. . . 4 |- -. x e. (/)
2	1	biorfi 408	. . 3 |- ( x e. A <-> ( x e. A \/ x e. (/) ) )
3	2	bicomi 205	. 2 |- ( ( x e. A \/ x e. (/) ) <-> x e. A )
4	3	uneqri 3605	1 |- ( A u. (/) ) = A

Syntax hints:   \/ wo 369   = wceq 1437   e. wcel 1867   u. cun 3431   (/)c0 3758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-dif 3436  df-un 3438  df-nul 3759

This theorem is referenced by:  csbun  3823  un00  3825  disjssun  3847  difun2  3872  difdifdir  3880  disjpr2  4056  prprc1  4104  diftpsn3  4132  sspr  4157  sstp  4158  symdif0  4370  symdifv  4371  symdifid  4372  iununi  4381  unidif0  4589  difxp1  5273  difxp2  5274  suc0  5507  sucprc  5508  fresaun  5762  fresaunres2  5763  fvssunirn  5895  fvun1  5943  fndifnfp  6099  fvunsn  6102  fvsnun1  6105  fvsnun2  6106  fsnunfv  6110  fsnunres  6111  funiunfv  6159  fnsuppeq0  6945  wfrlem14  7048  oev2  7224  oarec  7262  undifixp  7557  domss2  7728  domunfican  7841  kmlem2  8570  kmlem3  8571  kmlem11  8579  cda0en  8598  cdaassen  8601  ackbij1lem1  8639  ackbij1lem13  8651  fin1a2lem10  8828  fin1a2lem12  8830  axdc3lem4  8872  ttukeylem6  8933  alephadd  8991  fpwwe2lem13  9056  prunioo  11748  fzsuc2  11840  fseq1p1m1  11855  hashgval  12504  hashinf  12506  hashfun  12593  sadid1  14405  lcmfunsnlem  14574  lcmfun  14578  vdwap1  14879  setsres  15103  setsid  15116  mreexexlem3d  15496  mreexdomd  15499  pwssplit1  18210  lspsnat  18296  lsppratlem3  18300  opsrtoslem2  18636  indistopon  19940  indistps  19950  indistps2  19951  restcld  20112  neitr  20120  refun0  20454  filcon  20822  ufildr  20870  restmetu  21509  ovolioo  22395  itgsplitioo  22669  plyeq0  23030  birthdaylem2  23740  lgsquadlem2  24143  constr3pthlem1  25225  ex-dif  25715  ex-in  25717  ex-res  25733  iunxdif3  28011  difres  28047  imadifxp  28048  ofpreima2  28106  padct  28147  difico  28198  locfinref  28504  sigaclfu2  28779  prsiga  28789  unelldsys  28816  measun  28869  difelcarsg  28968  carsgclctunlem1  28975  carsggect  28976  eulerpartlemt  29027  eulerpartgbij  29028  ballotlemfp1  29147  indispcon  29742  nofulllem1  30373  nofulllem2  30374  onint1  30891  bj-pr21val  31353  bj-pr22val  31359  poimirlem3  31647  poimirlem5  31649  poimirlem10  31654  poimirlem15  31659  poimirlem22  31666  poimirlem23  31667  poimirlem28  31672  padd01  33085  padd02  33086  pclfinclN  33224  mapfzcons1  35268  fzsplit1nn0  35305  diophrw  35310  eldioph2lem1  35311  eldioph2lem2  35312  diophren  35365  pwssplit4  35657  0un  37031  dvmptfprodlem  37392  prsal  37730  caratheodorylem1  37860  fzopredsuc  38123  aacllem  39314