Theorem un0 4335

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 4279	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 940	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 224	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4097	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3888  ∅c0 4274

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-un 3895  df-nul 4275

This theorem is referenced by:  0un  4337  csbun  4382  un00  4386  disjssun  4409  difun2  4422  difdifdir  4432  disjpr2  4658  prprc1  4710  diftpsn3  4746  symdif0  5028  symdifid  5030  iununi  5042  unidif0  5297  relresdm1  5992  difxp1  6123  difxp2  6124  suc0  6394  sucprc  6395  fresaun  6705  fresaunres2  6706  fvun1  6925  fndifnfp  7124  fvunsn  7127  fvsnun1  7130  fvsnun2  7131  fsnunfv  7135  fsnunres  7136  funiunfv  7196  fnsuppeq0  8135  frrlem12  8240  oev2  8451  oarec  8490  undifixp  8875  domss2  9067  unfi  9098  domunfican  9225  kmlem2  10065  kmlem3  10066  kmlem11  10074  dju0en  10089  djuassen  10092  ackbij1lem1  10132  ackbij1lem13  10144  fin1a2lem10  10322  fin1a2lem12  10324  axdc3lem4  10366  ttukeylem6  10427  alephadd  10491  fpwwe2lem12  10556  indconst1  12163  prunioo  13425  fzsuc2  13527  fseq1p1m1  13543  hashgval  14286  hashinf  14288  hashfun  14390  sadid1  16428  lcmfunsnlem  16601  lcmfun  16605  vdwap1  16939  setsres  17139  setsid  17168  mreexexlem3d  17603  mreexdomd  17606  pwmndid  18898  pwmnd  18899  pwssplit1  21046  lspsnat  21135  lsppratlem3  21139  opsrtoslem2  22044  indistopon  22976  indistps  22986  indistps2  22987  restcld  23147  neitr  23155  refun0  23490  filconn  23858  ufildr  23906  restmetu  24545  ovolioo  25545  itgsplitioo  25815  plyeq0  26186  birthdaylem2  26929  lgsquadlem2  27358  noextendseq  27645  nosupbnd2lem1  27693  noinfbnd2lem1  27708  noetasuplem2  27712  noetasuplem3  27713  noetasuplem4  27714  noetainflem2  27716  bday1  27820  lrold  27903  addsrid  27970  negsproplem2  28035  negsproplem6  28039  muls01  28118  mulsrid  28119  mulsproplem2  28123  mulsproplem3  28124  mulsproplem4  28125  mulsproplem12  28133  mulsproplem13  28134  mulsproplem14  28135  onleft  28266  ltonold  28267  oncutlt  28270  oniso  28277  bdayons  28282  onaddscl  28283  onmulscl  28284  n0cut  28340  n0bday  28358  bdayn0p1  28375  0reno  28502  1reno  28503  ex-dif  30508  ex-in  30510  ex-res  30526  difres  32685  imadifxp  32686  ofpreima2  32754  coprprop  32787  padct  32806  difico  32871  tocycf  33193  tocyc01  33194  elrgspnlem4  33321  esplyind  33734  constrextdg2lem  33908  locfinref  34001  sigaclfu2  34281  prsiga  34291  unelldsys  34318  measun  34371  difelcarsg  34470  carsgclctunlem1  34477  carsggect  34478  eulerpartlemt  34531  eulerpartgbij  34532  ballotlemfp1  34652  fineqvac  35276  indispconn  35432  onint1  36647  bj-pr21val  37336  bj-funun  37582  lindsdom  37949  poimirlem3  37958  poimirlem5  37960  poimirlem10  37965  poimirlem15  37970  poimirlem22  37977  poimirlem23  37978  poimirlem28  37983  padd01  40271  padd02  40272  pclfinclN  40410  mapfzcons1  43163  fzsplit1nn0  43200  diophrw  43205  eldioph2lem1  43206  eldioph2lem2  43207  diophren  43259  pwssplit4  43535  mnuprdlem1  44717  dvmptfprodlem  46390  caratheodorylem1  46972  isomenndlem  46976  fzopredsuc  47784  clnbgr0edg  48325  tposrescnv  49366  tposres2  49367  tposres3  49368  aacllem  50288