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

Theorem un0 3914
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 3873 . . . 4 ¬ 𝑥 ∈ ∅
21biorfi 420 . . 3 (𝑥𝐴 ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 212 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥𝐴)
43uneqri 3712 1 (𝐴 ∪ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wo 381   = wceq 1474  wcel 1975  cun 3533  c0 3869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-dif 3538  df-un 3540  df-nul 3870
This theorem is referenced by:  csbun  3956  un00  3958  disjssun  3983  difun2  3995  difdifdir  4003  disjpr2  4189  disjpr2OLD  4190  prprc1  4238  diftpsn3  4268  diftpsn3OLD  4269  sspr  4297  sstp  4298  symdif0  4523  symdifv  4524  symdifid  4525  iunxdif3  4532  iununi  4536  unidif0  4755  difxp1  5460  difxp2  5461  suc0  5698  sucprc  5699  fresaun  5969  fresaunres2  5970  fvssunirn  6108  fvun1  6160  fndifnfp  6321  fvunsn  6324  fvsnun1  6327  fvsnun2  6328  fsnunfv  6332  fsnunres  6333  funiunfv  6384  fnsuppeq0  7183  wfrlem14  7288  oev2  7463  oarec  7502  undifixp  7803  domss2  7977  domunfican  8091  kmlem2  8829  kmlem3  8830  kmlem11  8838  cda0en  8857  cdaassen  8860  ackbij1lem1  8898  ackbij1lem13  8910  fin1a2lem10  9087  fin1a2lem12  9089  axdc3lem4  9131  ttukeylem6  9192  alephadd  9251  fpwwe2lem13  9316  prunioo  12124  fzsuc2  12219  fseq1p1m1  12234  hashgval  12933  hashinf  12935  hashfun  13032  sadid1  14970  lcmfunsnlem  15134  lcmfun  15138  vdwap1  15461  setsres  15671  setsid  15684  mreexexlem3d  16071  mreexdomd  16075  pwssplit1  18822  lspsnat  18908  lsppratlem3  18912  opsrtoslem2  19248  indistopon  20553  indistps  20563  indistps2  20564  restcld  20724  neitr  20732  refun0  21066  filcon  21435  ufildr  21483  restmetu  22122  ovolioo  23056  itgsplitioo  23323  plyeq0  23684  birthdaylem2  24392  lgsquadlem2  24819  constr3pthlem1  25945  ex-dif  26434  ex-in  26436  ex-res  26452  difres  28597  imadifxp  28598  ofpreima2  28651  padct  28687  difico  28737  locfinref  29038  sigaclfu2  29313  prsiga  29323  unelldsys  29350  measun  29403  difelcarsg  29501  carsgclctunlem1  29508  carsggect  29509  eulerpartlemt  29562  eulerpartgbij  29563  ballotlemfp1  29682  indispcon  30272  nofulllem1  30903  nofulllem2  30904  onint1  31420  bj-pr21val  31993  bj-pr22val  31999  lindsdom  32372  poimirlem3  32381  poimirlem5  32383  poimirlem10  32388  poimirlem15  32393  poimirlem22  32400  poimirlem23  32401  poimirlem28  32406  padd01  33914  padd02  33915  pclfinclN  34053  mapfzcons1  36097  fzsplit1nn0  36134  diophrw  36139  eldioph2lem1  36140  eldioph2lem2  36141  diophren  36194  pwssplit4  36476  0un  38039  dvmptfprodlem  38634  prsal  39014  caratheodorylem1  39216  isomenndlem  39220  fzopredsuc  39747  aacllem  42315
  Copyright terms: Public domain W3C validator