MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  un0 Unicode version

Theorem un0 3644
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.
StepHypRef Expression
1 noel 3624 . . . 4  |-  -.  x  e.  (/)
21biorfi 397 . . 3  |-  ( x  e.  A  <->  ( x  e.  A  \/  x  e.  (/) ) )
32bicomi 194 . 2  |-  ( ( x  e.  A  \/  x  e.  (/) )  <->  x  e.  A )
43uneqri 3481 1  |-  ( A  u.  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    \/ wo 358    = wceq 1652    e. wcel 1725    u. cun 3310   (/)c0 3620
This theorem is referenced by:  un00  3655  disjssun  3677  difun2  3699  difdifdir  3707  disjpr2  3862  prprc1  3906  diftpsn3  3929  sspr  3954  sstp  3955  iununi  4167  unidif0  4364  suc0  4647  sucprc  4648  fresaun  5605  fresaunres2  5606  fvssunirn  5745  fvun1  5785  fvunsn  5916  fvsnun1  5919  fvsnun2  5920  fsnunfv  5924  fsnunres  5925  fnsuppeq0  5944  funiunfv  5986  difxp1  6372  difxp2  6373  oev2  6758  oarec  6796  undifixp  7089  domss2  7257  domunfican  7370  kmlem2  8020  kmlem3  8021  kmlem11  8029  cda0en  8048  cdaassen  8051  ackbij1lem1  8089  ackbij1lem13  8101  fin1a2lem10  8278  fin1a2lem12  8280  axdc3lem4  8322  ttukeylem6  8383  alephadd  8441  fpwwe2lem13  8506  prunioo  11014  fzsuc2  11093  fseq1p1m1  11110  hashgval  11609  hashinf  11611  hashfun  11688  sadid1  12968  vdwap1  13333  setsres  13483  setsid  13496  mreexexlem3d  13859  mreexdomd  13862  lspsnat  16205  lsppratlem3  16209  opsrtoslem2  16533  indistopon  17053  indistps  17063  indistps2  17064  restcld  17224  neitr  17232  filcon  17903  ufildr  17951  restmetu  18605  ovolioo  19450  itgsplitioo  19717  plyeq0  20118  birthdaylem2  20779  lgsquadlem2  21127  constr3pthlem1  21630  ex-dif  21719  ex-in  21721  ex-res  21737  imadifxp  24026  fmptpr  24050  difico  24134  sigaclfu2  24492  prsiga  24502  measun  24553  sibfof  24642  ballotlemfp1  24737  indispcon  24909  wfrlem14  25524  nofulllem1  25611  nofulllem2  25612  symdif0  25623  symdifV  25624  symdifid  25625  onint1  26147  fndifnfp  26674  mapfzcons1  26710  fzsplit1nn0  26749  diophrw  26754  eldioph2lem1  26755  eldioph2lem2  26756  diophren  26811  pwssplit1  27103  pwssplit4  27106  padd01  30447  padd02  30448  pclfinclN  30586
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-un 3317  df-nul 3621
  Copyright terms: Public domain W3C validator