Theorem uni0 4893

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 5255. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2190. (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 490	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1819	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4867	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 325	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4306	1 ⊢ ∪ ∅ = ∅

Syntax hints:   ∧ wa 399   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∅c0 4285  ∪ cuni 4864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3907  df-nul 4286  df-uni 4865

This theorem is referenced by:  csbuni  4895  uniintsn  4942  iununi  5055  unisn2  5261  eqsnuniex  5317  opswap  6212  unixp0  6266  unixpid  6267  unizlim  6466  iotanul  6497  funfv  6950  dffv2  6958  1stval  7968  2ndval  7969  1stnpr  7970  2ndnpr  7971  1st0  7972  2nd0  7973  1st2val  7994  2nd2val  7995  brtpos0  8208  tpostpos  8221  nnunifi  9231  supval2  9398  sup00  9408  infeq5  9589  rankuni  9818  rankxplim3  9836  iunfictbso  10067  cflim2  10217  fin1a2lem11  10364  itunisuc  10373  itunitc  10375  ttukeylem4  10466  relexpfldd  15060  incexclem  15849  arwval  18059  dprdsn  20061  zrhval  21539  0opn  22944  indistopon  23041  mretopd  23132  hauscmplem  23446  cmpfi  23448  comppfsc  23572  alexsublem  24084  alexsubALTlem2  24088  ptcmplem2  24093  lebnumlem3  25005  old0  27909  made0  27933  locfinref  34099  prsiga  34389  sigapildsys  34420  dya2iocuni  34541  fiunelcarsg  34574  carsgclctunlem1  34575  carsgclctunlem3  34578  fissorduni  35349  fineqvnttrclselem1  35381  wevgblacfn  35418  nnuni  36041  unisnif  36237  limsucncmpi  36769  heicant  38118  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  mbfresfi  38129  onov0suclim  43815  stoweidlem35  46573  stoweidlem39  46577  prsal  46856  issalnnd  46883  ismeannd  47005  caragenunicl  47062  isomennd  47069  dftpos5  49459  ipolub0  49577