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

Theorem un0 3958
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 3911 . . . 4 ¬ 𝑥 ∈ ∅
21biorfi 422 . . 3 (𝑥𝐴 ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 214 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥𝐴)
43uneqri 3747 1 (𝐴 ∪ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wo 383   = wceq 1481  wcel 1988  cun 3565  c0 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-un 3572  df-nul 3908
This theorem is referenced by:  csbun  4000  un00  4002  disjssun  4027  difun2  4039  difdifdir  4047  disjpr2  4239  disjpr2OLD  4240  prprc1  4291  diftpsn3  4323  diftpsn3OLD  4324  sspr  4357  sstp  4358  symdif0  4588  symdifv  4589  symdifid  4590  iunxdif3  4597  iununi  4601  unidif0  4829  difxp1  5547  difxp2  5548  suc0  5787  sucprc  5788  fresaun  6062  fresaunres2  6063  fvssunirn  6204  fvun1  6256  fndifnfp  6427  fvunsn  6430  fvsnun1  6433  fvsnun2  6434  fsnunfv  6438  fsnunres  6439  funiunfv  6491  fnsuppeq0  7308  wfrlem14  7413  oev2  7588  oarec  7627  undifixp  7929  domss2  8104  domunfican  8218  kmlem2  8958  kmlem3  8959  kmlem11  8967  cda0en  8986  cdaassen  8989  ackbij1lem1  9027  ackbij1lem13  9039  fin1a2lem10  9216  fin1a2lem12  9218  axdc3lem4  9260  ttukeylem6  9321  alephadd  9384  fpwwe2lem13  9449  prunioo  12286  fzsuc2  12383  fseq1p1m1  12398  hashgval  13103  hashinf  13105  hashfun  13207  sadid1  15171  lcmfunsnlem  15335  lcmfun  15339  vdwap1  15662  setsres  15882  setsid  15895  mreexexlem3d  16287  mreexdomd  16291  pwssplit1  19040  lspsnat  19126  lsppratlem3  19130  opsrtoslem2  19466  indistopon  20786  indistps  20796  indistps2  20797  restcld  20957  neitr  20965  refun0  21299  filconn  21668  ufildr  21716  restmetu  22356  ovolioo  23317  itgsplitioo  23585  plyeq0  23948  birthdaylem2  24660  lgsquadlem2  25087  ex-dif  27250  ex-in  27252  ex-res  27268  difres  29385  imadifxp  29386  funresdm1  29388  ofpreima2  29440  padct  29471  difico  29519  locfinref  29882  sigaclfu2  30158  prsiga  30168  unelldsys  30195  measun  30248  difelcarsg  30346  carsgclctunlem1  30353  carsggect  30354  eulerpartlemt  30407  eulerpartgbij  30408  ballotlemfp1  30527  indispconn  31190  noextendseq  31794  nosupbnd2lem1  31835  noetalem2  31838  noetalem3  31839  onint1  32423  bj-pr21val  32976  bj-pr22val  32982  lindsdom  33374  poimirlem3  33383  poimirlem5  33385  poimirlem10  33390  poimirlem15  33395  poimirlem22  33402  poimirlem23  33403  poimirlem28  33408  padd01  34916  padd02  34917  pclfinclN  35055  mapfzcons1  37099  fzsplit1nn0  37136  diophrw  37141  eldioph2lem1  37142  eldioph2lem2  37143  diophren  37196  pwssplit4  37478  0un  39035  dvmptfprodlem  39922  prsal  40301  caratheodorylem1  40503  isomenndlem  40507  fzopredsuc  41096  aacllem  42312
  Copyright terms: Public domain W3C validator