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

Theorem un0 4348
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 4300 . . . 4 ¬ 𝑥 ∈ ∅
21biorfi 934 . . 3 (𝑥𝐴 ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 225 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥𝐴)
43uneqri 4131 1 (𝐴 ∪ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wo 843   = wceq 1530  wcel 2107  cun 3938  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-dif 3943  df-un 3945  df-nul 4296
This theorem is referenced by:  0un  4350  csbun  4394  un00  4397  disjssun  4420  difun2  4432  difdifdir  4440  disjpr2  4648  prprc1  4700  diftpsn3  4734  sspr  4765  sstp  4766  symdif0  5004  symdifv  5005  symdifid  5006  iunxdif3  5014  iununi  5018  unidif0  5257  difxp1  6020  difxp2  6021  suc0  6263  sucprc  6264  fresaun  6546  fresaunres2  6547  fvssunirn  6696  fvun1  6751  fndifnfp  6934  fvunsn  6937  fvsnun1  6940  fvsnun2  6941  fsnunfv  6945  fsnunres  6946  funiunfv  7001  fnsuppeq0  7849  wfrlem14  7959  oev2  8139  oarec  8178  undifixp  8487  domss2  8665  domunfican  8780  kmlem2  9566  kmlem3  9567  kmlem11  9575  dju0en  9590  djuassen  9593  ackbij1lem1  9631  ackbij1lem13  9643  fin1a2lem10  9820  fin1a2lem12  9822  axdc3lem4  9864  ttukeylem6  9925  alephadd  9988  fpwwe2lem13  10053  prunioo  12857  fzsuc2  12955  fseq1p1m1  12971  hashgval  13683  hashinf  13685  hashfun  13788  sadid1  15807  lcmfunsnlem  15975  lcmfun  15979  vdwap1  16303  setsres  16515  setsid  16528  mreexexlem3d  16907  mreexdomd  16910  pwssplit1  19751  lspsnat  19837  lsppratlem3  19841  opsrtoslem2  20184  indistopon  21528  indistps  21538  indistps2  21539  restcld  21699  neitr  21707  refun0  22042  filconn  22410  ufildr  22458  restmetu  23098  ovolioo  24087  itgsplitioo  24356  plyeq0  24719  birthdaylem2  25447  lgsquadlem2  25874  ex-dif  28119  ex-in  28121  ex-res  28137  difres  30268  imadifxp  30269  funresdm1  30273  ofpreima2  30329  coprprop  30351  padct  30371  difico  30422  tocycf  30676  tocyc01  30677  locfinref  30994  sigaclfu2  31269  prsiga  31279  unelldsys  31306  measun  31359  difelcarsg  31457  carsgclctunlem1  31464  carsggect  31465  eulerpartlemt  31518  eulerpartgbij  31519  ballotlemfp1  31638  indispconn  32368  frrlem12  33021  noextendseq  33061  nosupbnd2lem1  33102  noetalem2  33105  noetalem3  33106  onint1  33684  bj-pr21val  34212  bj-funun  34416  lindsdom  34756  poimirlem3  34765  poimirlem5  34767  poimirlem10  34772  poimirlem15  34777  poimirlem22  34784  poimirlem23  34785  poimirlem28  34790  padd01  36817  padd02  36818  pclfinclN  36956  mapfzcons1  39182  fzsplit1nn0  39219  diophrw  39224  eldioph2lem1  39225  eldioph2lem2  39226  diophren  39278  pwssplit4  39557  mnuprdlem1  40476  dvmptfprodlem  42097  caratheodorylem1  42677  isomenndlem  42681  fzopredsuc  43392  aacllem  44737
  Copyright terms: Public domain W3C validator