Theorem uni0 4896

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 5260. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2194. (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 4293	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 491	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1823	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4870	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4310	1 ⊢ ∪ ∅ = ∅

Syntax hints:   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∅c0 4288  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3910  df-nul 4289  df-uni 4868

This theorem is referenced by:  csbuni  4898  uniintsn  4945  iununi  5060  unisn2  5266  eqsnuniex  5322  opswap  6219  unixp0  6273  unixpid  6274  unizlim  6474  iotanul  6505  funfv  6958  dffv2  6966  1stval  7976  2ndval  7977  1stnpr  7978  2ndnpr  7979  1st0  7980  2nd0  7981  1st2val  8002  2nd2val  8003  brtpos0  8217  tpostpos  8230  nnunifi  9239  supval2  9403  sup00  9413  infeq5  9594  rankuni  9823  rankxplim3  9841  iunfictbso  10086  cflim2  10235  fin1a2lem11  10382  itunisuc  10391  itunitc  10393  ttukeylem4  10484  relexpfldd  15075  incexclem  15878  arwval  18088  dprdsn  20096  zrhval  21614  0opn  23018  indistopon  23115  mretopd  23206  hauscmplem  23520  cmpfi  23522  comppfsc  23646  alexsublem  24158  alexsubALTlem2  24162  ptcmplem2  24167  lebnumlem3  25079  old0  27986  made0  28010  locfinref  34143  prsiga  34433  sigapildsys  34464  dya2iocuni  34585  fiunelcarsg  34618  carsgclctunlem1  34619  carsgclctunlem3  34622  fissorduni  35390  fineqvnttrclselem1  35424  wevgblacfn  35461  nnuni  36085  unisnif  36281  limsucncmpi  36813  heicant  38161  ovoliunnfl  38168  voliunnfl  38170  volsupnfl  38171  mbfresfi  38172  onov0suclim  43858  stoweidlem35  46608  stoweidlem39  46612  prsal  46891  issalnnd  46918  ismeannd  47040  caragenunicl  47097  isomennd  47104  dftpos5  49504  ipolub0  49622