Theorem uni0 4891

Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Contributed by NM, 16-Sep-1993.) Remove use of ax-nul 5251. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2162. (Revised by TM, 1-Feb-2026.)

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4290	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 486	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1801	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4866	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4306	1 ⊢ ∪ ∅ = ∅

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∅c0 4285  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-nul 4286  df-uni 4864

This theorem is referenced by:  csbuni  4893  uniintsn  4940  iununi  5054  unisn2  5257  eqsnuniex  5306  opswap  6187  unixp0  6241  unixpid  6242  unizlim  6441  iotanul  6472  funfv  6921  dffv2  6929  1stval  7935  2ndval  7936  1stnpr  7937  2ndnpr  7938  1st0  7939  2nd0  7940  1st2val  7961  2nd2val  7962  brtpos0  8175  tpostpos  8188  nnunifi  9191  supval2  9358  sup00  9368  infeq5  9546  rankuni  9775  rankxplim3  9793  iunfictbso  10024  cflim2  10173  fin1a2lem11  10320  itunisuc  10329  itunitc  10331  ttukeylem4  10422  relexpfldd  14973  incexclem  15759  arwval  17967  dprdsn  19967  zrhval  21462  0opn  22848  indistopon  22945  mretopd  23036  hauscmplem  23350  cmpfi  23352  comppfsc  23476  alexsublem  23988  alexsubALTlem2  23992  ptcmplem2  23997  lebnumlem3  24918  old0  27835  made0  27859  locfinref  33998  prsiga  34288  sigapildsys  34319  dya2iocuni  34440  fiunelcarsg  34473  carsgclctunlem1  34474  carsgclctunlem3  34477  fissorduni  35246  fineqvnttrclselem1  35277  wevgblacfn  35303  nnuni  35921  unisnif  36117  limsucncmpi  36639  heicant  37852  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  mbfresfi  37863  onov0suclim  43512  stoweidlem35  46275  stoweidlem39  46279  prsal  46558  issalnnd  46585  ismeannd  46707  caragenunicl  46764  isomennd  46771  dftpos5  49115  ipolub0  49233