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

Theorem un0 4165
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 4120 . . . 4 ¬ 𝑥 ∈ ∅
21biorfi 953 . . 3 (𝑥𝐴 ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 215 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥𝐴)
43uneqri 3954 1 (𝐴 ∪ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wo 865   = wceq 1637  wcel 2156  cun 3767  c0 4116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-dif 3772  df-un 3774  df-nul 4117
This theorem is referenced by:  csbun  4207  un00  4209  disjssun  4232  difun2  4244  difdifdir  4252  disjpr2  4440  prprc1  4491  diftpsn3  4523  sspr  4554  sstp  4555  symdif0  4789  symdifv  4790  symdifid  4791  iunxdif3  4798  iununi  4802  unidif0  5030  difxp1  5770  difxp2  5771  suc0  6012  sucprc  6013  fresaun  6290  fresaunres2  6291  fvssunirn  6437  fvun1  6490  fndifnfp  6667  fvunsn  6670  fvsnun1  6673  fvsnun2  6674  fsnunfv  6678  fsnunres  6679  funiunfv  6730  fnsuppeq0  7558  wfrlem14  7664  oev2  7840  oarec  7879  undifixp  8181  domss2  8358  domunfican  8472  kmlem2  9258  kmlem3  9259  kmlem11  9267  cda0en  9286  cdaassen  9289  ackbij1lem1  9327  ackbij1lem13  9339  fin1a2lem10  9516  fin1a2lem12  9518  axdc3lem4  9560  ttukeylem6  9621  alephadd  9684  fpwwe2lem13  9749  prunioo  12524  fzsuc2  12621  fseq1p1m1  12637  hashgval  13340  hashinf  13342  hashfun  13441  sadid1  15409  lcmfunsnlem  15573  lcmfun  15577  vdwap1  15898  setsres  16112  setsid  16125  mreexexlem3d  16511  mreexdomd  16514  pwssplit1  19266  lspsnat  19353  lsppratlem3  19358  opsrtoslem2  19693  indistopon  21019  indistps  21029  indistps2  21030  restcld  21190  neitr  21198  refun0  21532  filconn  21900  ufildr  21948  restmetu  22588  ovolioo  23549  itgsplitioo  23818  plyeq0  24181  birthdaylem2  24893  lgsquadlem2  25320  ex-dif  27611  ex-in  27613  ex-res  27629  difres  29738  imadifxp  29739  funresdm1  29741  ofpreima2  29793  padct  29824  difico  29872  locfinref  30233  sigaclfu2  30509  prsiga  30519  unelldsys  30546  measun  30599  difelcarsg  30697  carsgclctunlem1  30704  carsggect  30705  eulerpartlemt  30758  eulerpartgbij  30759  ballotlemfp1  30878  indispconn  31539  noextendseq  32141  nosupbnd2lem1  32182  noetalem2  32185  noetalem3  32186  onint1  32765  bj-pr21val  33311  bj-pr22val  33317  lindsdom  33716  poimirlem3  33725  poimirlem5  33727  poimirlem10  33732  poimirlem15  33737  poimirlem22  33744  poimirlem23  33745  poimirlem28  33750  padd01  35591  padd02  35592  pclfinclN  35730  mapfzcons1  37782  fzsplit1nn0  37819  diophrw  37824  eldioph2lem1  37825  eldioph2lem2  37826  diophren  37879  pwssplit4  38160  0un  39708  dvmptfprodlem  40639  prsal  41017  caratheodorylem1  41222  isomenndlem  41226  fzopredsuc  41908  aacllem  43118
  Copyright terms: Public domain W3C validator