Theorem uni0 4879

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 5241. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2163. (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 4279	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 486	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1802	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4854	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4295	1 ⊢ ∪ ∅ = ∅

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4274  ∪ cuni 4851

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-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-nul 4275  df-uni 4852

This theorem is referenced by:  csbuni  4881  uniintsn  4928  iununi  5042  unisn2  5247  eqsnuniex  5298  opswap  6187  unixp0  6241  unixpid  6242  unizlim  6441  iotanul  6472  funfv  6921  dffv2  6929  1stval  7937  2ndval  7938  1stnpr  7939  2ndnpr  7940  1st0  7941  2nd0  7942  1st2val  7963  2nd2val  7964  brtpos0  8176  tpostpos  8189  nnunifi  9194  supval2  9361  sup00  9371  infeq5  9549  rankuni  9778  rankxplim3  9796  iunfictbso  10027  cflim2  10176  fin1a2lem11  10323  itunisuc  10332  itunitc  10334  ttukeylem4  10425  relexpfldd  15003  incexclem  15792  arwval  18001  dprdsn  20004  zrhval  21497  0opn  22879  indistopon  22976  mretopd  23067  hauscmplem  23381  cmpfi  23383  comppfsc  23507  alexsublem  24019  alexsubALTlem2  24023  ptcmplem2  24028  lebnumlem3  24940  old0  27845  made0  27869  locfinref  34001  prsiga  34291  sigapildsys  34322  dya2iocuni  34443  fiunelcarsg  34476  carsgclctunlem1  34477  carsgclctunlem3  34480  fissorduni  35249  fineqvnttrclselem1  35281  wevgblacfn  35307  nnuni  35925  unisnif  36121  limsucncmpi  36643  heicant  37990  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  mbfresfi  38001  onov0suclim  43720  stoweidlem35  46481  stoweidlem39  46485  prsal  46764  issalnnd  46791  ismeannd  46913  caragenunicl  46970  isomennd  46977  dftpos5  49361  ipolub0  49479