Theorem un0 4298

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.

Step	Hyp	Ref	Expression
1		noel 4247	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 936	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4078	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ∪ cun 3879  ∅c0 4243

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-un 3886  df-nul 4244

This theorem is referenced by:  0un  4300  csbun  4346  un00  4350  disjssun  4375  difun2  4387  difdifdir  4395  disjpr2  4609  prprc1  4661  diftpsn3  4695  sspr  4726  sstp  4727  symdif0  4970  symdifv  4971  symdifid  4972  iunxdif3  4980  iununi  4984  unidif0  5225  difxp1  5989  difxp2  5990  suc0  6233  sucprc  6234  fresaun  6523  fresaunres2  6524  fvssunirn  6674  fvun1  6729  fndifnfp  6915  fvunsn  6918  fvsnun1  6921  fvsnun2  6922  fsnunfv  6926  fsnunres  6927  funiunfv  6985  fnsuppeq0  7841  wfrlem14  7951  oev2  8131  oarec  8171  undifixp  8481  domss2  8660  domunfican  8775  kmlem2  9562  kmlem3  9563  kmlem11  9571  dju0en  9586  djuassen  9589  ackbij1lem1  9631  ackbij1lem13  9643  fin1a2lem10  9820  fin1a2lem12  9822  axdc3lem4  9864  ttukeylem6  9925  alephadd  9988  fpwwe2lem13  10053  prunioo  12859  fzsuc2  12960  fseq1p1m1  12976  hashgval  13689  hashinf  13691  hashfun  13794  sadid1  15807  lcmfunsnlem  15975  lcmfun  15979  vdwap1  16303  setsres  16517  setsid  16530  mreexexlem3d  16909  mreexdomd  16912  pwmndid  18093  pwmnd  18094  pwssplit1  19824  lspsnat  19910  lsppratlem3  19914  opsrtoslem2  20724  indistopon  21606  indistps  21616  indistps2  21617  restcld  21777  neitr  21785  refun0  22120  filconn  22488  ufildr  22536  restmetu  23177  ovolioo  24172  itgsplitioo  24441  plyeq0  24808  birthdaylem2  25538  lgsquadlem2  25965  ex-dif  28208  ex-in  28210  ex-res  28226  difres  30363  imadifxp  30364  funresdm1  30368  ofpreima2  30429  coprprop  30459  padct  30481  difico  30532  tocycf  30809  tocyc01  30810  locfinref  31194  sigaclfu2  31490  prsiga  31500  unelldsys  31527  measun  31580  difelcarsg  31678  carsgclctunlem1  31685  carsggect  31686  eulerpartlemt  31739  eulerpartgbij  31740  ballotlemfp1  31859  indispconn  32594  frrlem12  33247  noextendseq  33287  nosupbnd2lem1  33328  noetalem2  33331  noetalem3  33332  onint1  33910  bj-pr21val  34449  bj-funun  34667  lindsdom  35051  poimirlem3  35060  poimirlem5  35062  poimirlem10  35067  poimirlem15  35072  poimirlem22  35079  poimirlem23  35080  poimirlem28  35085  padd01  37107  padd02  37108  pclfinclN  37246  metakunt24  39373  mapfzcons1  39658  fzsplit1nn0  39695  diophrw  39700  eldioph2lem1  39701  eldioph2lem2  39702  diophren  39754  pwssplit4  40033  mnuprdlem1  40980  dvmptfprodlem  42586  caratheodorylem1  43165  isomenndlem  43169  fzopredsuc  43880  aacllem  45329