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

Theorem un0 3654
Description: The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
un0  |-  ( A  u.  (/) )  =  A

Proof of Theorem un0
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 noel 3634 . . . 4  |-  -.  x  e.  (/)
21biorfi 398 . . 3  |-  ( x  e.  A  <->  ( x  e.  A  \/  x  e.  (/) ) )
32bicomi 195 . 2  |-  ( ( x  e.  A  \/  x  e.  (/) )  <->  x  e.  A )
43uneqri 3491 1  |-  ( A  u.  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1653    e. wcel 1726    u. cun 3320   (/)c0 3630
This theorem is referenced by:  un00  3665  disjssun  3687  difun2  3709  difdifdir  3717  disjpr2  3872  prprc1  3916  diftpsn3  3939  sspr  3964  sstp  3965  iununi  4178  unidif0  4375  suc0  4658  sucprc  4659  fresaun  5617  fresaunres2  5618  fvssunirn  5757  fvun1  5797  fvunsn  5928  fvsnun1  5931  fvsnun2  5932  fsnunfv  5936  fsnunres  5937  fnsuppeq0  5956  funiunfv  5998  difxp1  6384  difxp2  6385  oev2  6770  oarec  6808  undifixp  7101  domss2  7269  domunfican  7382  kmlem2  8036  kmlem3  8037  kmlem11  8045  cda0en  8064  cdaassen  8067  ackbij1lem1  8105  ackbij1lem13  8117  fin1a2lem10  8294  fin1a2lem12  8296  axdc3lem4  8338  ttukeylem6  8399  alephadd  8457  fpwwe2lem13  8522  prunioo  11030  fzsuc2  11109  fseq1p1m1  11127  hashgval  11626  hashinf  11628  hashfun  11705  sadid1  12985  vdwap1  13350  setsres  13500  setsid  13513  mreexexlem3d  13876  mreexdomd  13879  lspsnat  16222  lsppratlem3  16226  opsrtoslem2  16550  indistopon  17070  indistps  17080  indistps2  17081  restcld  17241  neitr  17249  filcon  17920  ufildr  17968  restmetu  18622  ovolioo  19467  itgsplitioo  19732  plyeq0  20135  birthdaylem2  20796  lgsquadlem2  21144  constr3pthlem1  21647  ex-dif  21736  ex-in  21738  ex-res  21754  imadifxp  24043  fmptpr  24067  difico  24151  sigaclfu2  24509  prsiga  24519  measun  24570  sibfof  24659  ballotlemfp1  24754  indispcon  24926  wfrlem14  25556  nofulllem1  25662  nofulllem2  25663  symdif0  25674  symdifV  25675  symdifid  25676  onint1  26204  fndifnfp  26751  mapfzcons1  26787  fzsplit1nn0  26826  diophrw  26831  eldioph2lem1  26832  eldioph2lem2  26833  diophren  26888  pwssplit1  27179  pwssplit4  27182  padd01  30682  padd02  30683  pclfinclN  30821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-un 3327  df-nul 3631
  Copyright terms: Public domain W3C validator