Theorem un0 3612

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 3592	. . . 4 |- -. x e. (/)
2	1	biorfi 397	. . 3 |- ( x e. A <-> ( x e. A \/ x e. (/) ) )
3	2	bicomi 194	. 2 |- ( ( x e. A \/ x e. (/) ) <-> x e. A )
4	3	uneqri 3449	1 |- ( A u. (/) ) = A

Syntax hints:   \/ wo 358   = wceq 1649   e. wcel 1721   u. cun 3278   (/)c0 3588

This theorem is referenced by:  un00  3623  disjssun  3645  difun2  3667  difdifdir  3675  disjpr2  3830  prprc1  3874  diftpsn3  3897  sspr  3922  sstp  3923  iununi  4135  unidif0  4332  suc0  4615  sucprc  4616  fresaun  5573  fresaunres2  5574  fvssunirn  5713  fvun1  5753  fvunsn  5884  fvsnun1  5887  fvsnun2  5888  fsnunfv  5892  fsnunres  5893  fnsuppeq0  5912  funiunfv  5954  difxp1  6340  difxp2  6341  oev2  6726  oarec  6764  undifixp  7057  domss2  7225  domunfican  7338  kmlem2  7987  kmlem3  7988  kmlem11  7996  cda0en  8015  cdaassen  8018  ackbij1lem1  8056  ackbij1lem13  8068  fin1a2lem10  8245  fin1a2lem12  8247  axdc3lem4  8289  ttukeylem6  8350  alephadd  8408  fpwwe2lem13  8473  prunioo  10981  fzsuc2  11060  fseq1p1m1  11077  hashgval  11576  hashinf  11578  hashfun  11655  sadid1  12935  vdwap1  13300  setsres  13450  setsid  13463  mreexexlem3d  13826  mreexdomd  13829  lspsnat  16172  lsppratlem3  16176  opsrtoslem2  16500  indistopon  17020  indistps  17030  indistps2  17031  restcld  17190  neitr  17198  filcon  17868  ufildr  17916  restmetu  18570  ovolioo  19415  itgsplitioo  19682  plyeq0  20083  birthdaylem2  20744  lgsquadlem2  21092  constr3pthlem1  21595  ex-dif  21684  ex-in  21686  ex-res  21702  imadifxp  23991  fmptpr  24015  difico  24099  sigaclfu2  24457  prsiga  24467  measun  24518  sibfof  24607  ballotlemfp1  24702  indispcon  24874  wfrlem14  25483  nofulllem1  25570  nofulllem2  25571  symdif0  25582  symdifV  25583  symdifid  25584  onint1  26103  fndifnfp  26627  mapfzcons1  26663  fzsplit1nn0  26702  diophrw  26707  eldioph2lem1  26708  eldioph2lem2  26709  diophren  26764  pwssplit1  27056  pwssplit4  27059  padd01  30293  padd02  30294  pclfinclN  30432

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-un 3285  df-nul 3589