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 4288 . . . 4 ¬ 𝑥 ∈ ∅
21biorfi 937 . . 3 (𝑥𝐴 ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 223 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥𝐴)
43uneqri 4109 1 (𝐴 ∪ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wo 845   = wceq 1541  wcel 2106  cun 3906  c0 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-dif 3911  df-un 3913  df-nul 4281
This theorem is referenced by:  0un  4350  csbun  4396  un00  4400  disjssun  4425  difun2  4438  difdifdir  4447  disjpr2  4672  prprc1  4724  diftpsn3  4760  sspr  4791  sstp  4792  symdif0  5043  symdifv  5044  symdifid  5045  iunxdif3  5053  iununi  5057  unidif0  5313  difxp1  6115  difxp2  6116  suc0  6390  sucprc  6391  fresaun  6710  fresaunres2  6711  fvssunirnOLD  6873  fvun1  6929  fndifnfp  7118  fvunsn  7121  fvsnun1  7124  fvsnun2  7125  fsnunfv  7129  fsnunres  7130  funiunfv  7191  fnsuppeq0  8115  frrlem12  8220  wfrlem14OLD  8260  oev2  8461  oarec  8501  undifixp  8830  domss2  9038  unfi  9074  domunfican  9222  kmlem2  10045  kmlem3  10046  kmlem11  10054  dju0en  10069  djuassen  10072  ackbij1lem1  10114  ackbij1lem13  10126  fin1a2lem10  10303  fin1a2lem12  10305  axdc3lem4  10347  ttukeylem6  10408  alephadd  10471  fpwwe2lem12  10536  prunioo  13352  fzsuc2  13453  fseq1p1m1  13469  hashgval  14187  hashinf  14189  hashfun  14291  sadid1  16308  lcmfunsnlem  16477  lcmfun  16481  vdwap1  16809  setsres  17010  setsid  17040  mreexexlem3d  17486  mreexdomd  17489  pwmndid  18706  pwmnd  18707  pwssplit1  20473  lspsnat  20559  lsppratlem3  20563  opsrtoslem2  21415  indistopon  22303  indistps  22313  indistps2  22314  restcld  22475  neitr  22483  refun0  22818  filconn  23186  ufildr  23234  restmetu  23878  ovolioo  24884  itgsplitioo  25154  plyeq0  25524  birthdaylem2  26254  lgsquadlem2  26681  noextendseq  26967  nosupbnd2lem1  27015  noinfbnd2lem1  27030  noetasuplem2  27034  noetasuplem3  27035  noetasuplem4  27036  noetainflem2  27038  bday1s  27122  lrold  27175  ex-dif  29196  ex-in  29198  ex-res  29214  difres  31347  imadifxp  31348  funresdm1  31352  ofpreima2  31411  coprprop  31440  padct  31462  difico  31512  tocycf  31792  tocyc01  31793  locfinref  32234  sigaclfu2  32532  prsiga  32542  unelldsys  32569  measun  32622  difelcarsg  32722  carsgclctunlem1  32729  carsggect  32730  eulerpartlemt  32783  eulerpartgbij  32784  ballotlemfp1  32903  fineqvac  33510  indispconn  33640  addsid1  34279  negsproplem2  34322  negsproplem6  34326  onint1  34859  bj-pr21val  35422  bj-funun  35661  lindsdom  36010  poimirlem3  36019  poimirlem5  36021  poimirlem10  36026  poimirlem15  36031  poimirlem22  36038  poimirlem23  36039  poimirlem28  36044  padd01  38212  padd02  38213  pclfinclN  38351  metakunt24  40538  mapfzcons1  40949  fzsplit1nn0  40986  diophrw  40991  eldioph2lem1  40992  eldioph2lem2  40993  diophren  41045  pwssplit4  41325  mnuprdlem1  42463  dvmptfprodlem  44086  caratheodorylem1  44668  isomenndlem  44672  fzopredsuc  45456  aacllem  47149
  Copyright terms: Public domain W3C validator