Theorem un0 4324

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 4264	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 936	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 223	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4085	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 844   = wceq 1539   ∈ wcel 2106   ∪ cun 3885  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257

This theorem is referenced by:  0un  4326  csbun  4372  un00  4376  disjssun  4401  difun2  4414  difdifdir  4422  disjpr2  4649  prprc1  4701  diftpsn3  4735  sspr  4766  sstp  4767  symdif0  5014  symdifv  5015  symdifid  5016  iunxdif3  5024  iununi  5028  unidif0  5282  difxp1  6068  difxp2  6069  suc0  6340  sucprc  6341  fresaun  6645  fresaunres2  6646  fvssunirn  6803  fvun1  6859  fndifnfp  7048  fvunsn  7051  fvsnun1  7054  fvsnun2  7055  fsnunfv  7059  fsnunres  7060  funiunfv  7121  fnsuppeq0  8008  frrlem12  8113  wfrlem14OLD  8153  oev2  8353  oarec  8393  undifixp  8722  domss2  8923  unfi  8955  domunfican  9087  kmlem2  9907  kmlem3  9908  kmlem11  9916  dju0en  9931  djuassen  9934  ackbij1lem1  9976  ackbij1lem13  9988  fin1a2lem10  10165  fin1a2lem12  10167  axdc3lem4  10209  ttukeylem6  10270  alephadd  10333  fpwwe2lem12  10398  prunioo  13213  fzsuc2  13314  fseq1p1m1  13330  hashgval  14047  hashinf  14049  hashfun  14152  sadid1  16175  lcmfunsnlem  16346  lcmfun  16350  vdwap1  16678  setsres  16879  setsid  16909  mreexexlem3d  17355  mreexdomd  17358  pwmndid  18575  pwmnd  18576  pwssplit1  20321  lspsnat  20407  lsppratlem3  20411  opsrtoslem2  21263  indistopon  22151  indistps  22161  indistps2  22162  restcld  22323  neitr  22331  refun0  22666  filconn  23034  ufildr  23082  restmetu  23726  ovolioo  24732  itgsplitioo  25002  plyeq0  25372  birthdaylem2  26102  lgsquadlem2  26529  ex-dif  28787  ex-in  28789  ex-res  28805  difres  30939  imadifxp  30940  funresdm1  30944  ofpreima2  31003  coprprop  31032  padct  31054  difico  31104  tocycf  31384  tocyc01  31385  locfinref  31791  sigaclfu2  32089  prsiga  32099  unelldsys  32126  measun  32179  difelcarsg  32277  carsgclctunlem1  32284  carsggect  32285  eulerpartlemt  32338  eulerpartgbij  32339  ballotlemfp1  32458  fineqvac  33066  indispconn  33196  noextendseq  33870  nosupbnd2lem1  33918  noinfbnd2lem1  33933  noetasuplem2  33937  noetasuplem3  33938  noetasuplem4  33939  noetainflem2  33941  bday1s  34025  lrold  34077  addsid1  34127  onint1  34638  bj-pr21val  35203  bj-funun  35423  lindsdom  35771  poimirlem3  35780  poimirlem5  35782  poimirlem10  35787  poimirlem15  35792  poimirlem22  35799  poimirlem23  35800  poimirlem28  35805  padd01  37825  padd02  37826  pclfinclN  37964  metakunt24  40148  mapfzcons1  40539  fzsplit1nn0  40576  diophrw  40581  eldioph2lem1  40582  eldioph2lem2  40583  diophren  40635  pwssplit4  40914  mnuprdlem1  41890  dvmptfprodlem  43485  caratheodorylem1  44064  isomenndlem  44068  fzopredsuc  44815  aacllem  46505