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

Theorem un0 4351
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 (𝐴 ∪ ∅) = 𝐴

Proof of Theorem un0
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 noel 4291 . . . 4 ¬ 𝑥 ∈ ∅
21biorfi 938 . . 3 (𝑥𝐴 ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 223 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥𝐴)
43uneqri 4112 1 (𝐴 ∪ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wo 846   = wceq 1542  wcel 2107  cun 3909  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-dif 3914  df-un 3916  df-nul 4284
This theorem is referenced by:  0un  4353  csbun  4399  un00  4403  disjssun  4428  difun2  4441  difdifdir  4450  disjpr2  4675  prprc1  4727  diftpsn3  4763  sspr  4794  sstp  4795  symdif0  5046  symdifv  5047  symdifid  5048  iunxdif3  5056  iununi  5060  unidif0  5316  difxp1  6118  difxp2  6119  suc0  6393  sucprc  6394  fresaun  6714  fresaunres2  6715  fvssunirnOLD  6877  fvun1  6933  fndifnfp  7123  fvunsn  7126  fvsnun1  7129  fvsnun2  7130  fsnunfv  7134  fsnunres  7135  funiunfv  7196  fnsuppeq0  8124  frrlem12  8229  wfrlem14OLD  8269  oev2  8470  oarec  8510  undifixp  8875  domss2  9083  unfi  9119  domunfican  9267  kmlem2  10092  kmlem3  10093  kmlem11  10101  dju0en  10116  djuassen  10119  ackbij1lem1  10161  ackbij1lem13  10173  fin1a2lem10  10350  fin1a2lem12  10352  axdc3lem4  10394  ttukeylem6  10455  alephadd  10518  fpwwe2lem12  10583  prunioo  13404  fzsuc2  13505  fseq1p1m1  13521  hashgval  14239  hashinf  14241  hashfun  14343  sadid1  16353  lcmfunsnlem  16522  lcmfun  16526  vdwap1  16854  setsres  17055  setsid  17085  mreexexlem3d  17531  mreexdomd  17534  pwmndid  18751  pwmnd  18752  pwssplit1  20535  lspsnat  20622  lsppratlem3  20626  opsrtoslem2  21479  indistopon  22367  indistps  22377  indistps2  22378  restcld  22539  neitr  22547  refun0  22882  filconn  23250  ufildr  23298  restmetu  23942  ovolioo  24948  itgsplitioo  25218  plyeq0  25588  birthdaylem2  26318  lgsquadlem2  26745  noextendseq  27031  nosupbnd2lem1  27079  noinfbnd2lem1  27094  noetasuplem2  27098  noetasuplem3  27099  noetasuplem4  27100  noetainflem2  27102  bday1s  27192  lrold  27248  addsrid  27298  negsproplem2  27349  negsproplem6  27353  muls01  27397  muls02  27398  mulsrid  27399  mulslid  27400  ex-dif  29409  ex-in  29411  ex-res  29427  difres  31564  imadifxp  31565  funresdm1  31569  ofpreima2  31628  coprprop  31660  padct  31683  difico  31733  tocycf  32015  tocyc01  32016  locfinref  32479  sigaclfu2  32777  prsiga  32787  unelldsys  32814  measun  32867  difelcarsg  32967  carsgclctunlem1  32974  carsggect  32975  eulerpartlemt  33028  eulerpartgbij  33029  ballotlemfp1  33148  fineqvac  33755  indispconn  33885  onint1  34967  bj-pr21val  35530  bj-funun  35769  lindsdom  36118  poimirlem3  36127  poimirlem5  36129  poimirlem10  36134  poimirlem15  36139  poimirlem22  36146  poimirlem23  36147  poimirlem28  36152  padd01  38320  padd02  38321  pclfinclN  38459  metakunt24  40646  mapfzcons1  41083  fzsplit1nn0  41120  diophrw  41125  eldioph2lem1  41126  eldioph2lem2  41127  diophren  41179  pwssplit4  41459  mnuprdlem1  42640  dvmptfprodlem  44271  caratheodorylem1  44853  isomenndlem  44857  fzopredsuc  45641  aacllem  47334
  Copyright terms: Public domain W3C validator