Theorem uni0 4878

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 4278	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 486	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1802	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4853	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4294	1 ⊢ ∪ ∅ = ∅

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-nul 4274  df-uni 4851

This theorem is referenced by:  csbuni  4880  uniintsn  4927  iununi  5041  unisn2  5247  eqsnuniex  5303  opswap  6193  unixp0  6247  unixpid  6248  unizlim  6447  iotanul  6478  funfv  6927  dffv2  6935  1stval  7944  2ndval  7945  1stnpr  7946  2ndnpr  7947  1st0  7948  2nd0  7949  1st2val  7970  2nd2val  7971  brtpos0  8183  tpostpos  8196  nnunifi  9201  supval2  9368  sup00  9378  infeq5  9558  rankuni  9787  rankxplim3  9805  iunfictbso  10036  cflim2  10185  fin1a2lem11  10332  itunisuc  10341  itunitc  10343  ttukeylem4  10434  relexpfldd  15012  incexclem  15801  arwval  18010  dprdsn  20013  zrhval  21487  0opn  22869  indistopon  22966  mretopd  23057  hauscmplem  23371  cmpfi  23373  comppfsc  23497  alexsublem  24009  alexsubALTlem2  24013  ptcmplem2  24018  lebnumlem3  24930  old0  27831  made0  27855  locfinref  33985  prsiga  34275  sigapildsys  34306  dya2iocuni  34427  fiunelcarsg  34460  carsgclctunlem1  34461  carsgclctunlem3  34464  fissorduni  35233  fineqvnttrclselem1  35265  wevgblacfn  35291  nnuni  35909  unisnif  36105  limsucncmpi  36627  heicant  37976  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  mbfresfi  37987  onov0suclim  43702  stoweidlem35  46463  stoweidlem39  46467  prsal  46746  issalnnd  46773  ismeannd  46895  caragenunicl  46952  isomennd  46959  dftpos5  49349  ipolub0  49467