Theorem uni0 4886

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-nul 4283  df-uni 4859

This theorem is referenced by:  csbuni  4888  uniintsn  4935  iununi  5049  unisn2  5252  eqsnuniex  5301  opswap  6181  unixp0  6235  unixpid  6236  unizlim  6435  iotanul  6466  funfv  6915  dffv2  6923  1stval  7929  2ndval  7930  1stnpr  7931  2ndnpr  7932  1st0  7933  2nd0  7934  1st2val  7955  2nd2val  7956  brtpos0  8169  tpostpos  8182  nnunifi  9182  supval2  9346  sup00  9356  infeq5  9534  rankuni  9763  rankxplim3  9781  iunfictbso  10012  cflim2  10161  fin1a2lem11  10308  itunisuc  10317  itunitc  10319  ttukeylem4  10410  relexpfldd  14959  incexclem  15745  arwval  17952  dprdsn  19952  zrhval  21446  0opn  22820  indistopon  22917  mretopd  23008  hauscmplem  23322  cmpfi  23324  comppfsc  23448  alexsublem  23960  alexsubALTlem2  23964  ptcmplem2  23969  lebnumlem3  24890  old0  27801  made0  27819  locfinref  33875  prsiga  34165  sigapildsys  34196  dya2iocuni  34317  fiunelcarsg  34350  carsgclctunlem1  34351  carsgclctunlem3  34354  fissorduni  35122  fineqvnttrclselem1  35162  wevgblacfn  35174  nnuni  35792  unisnif  35988  limsucncmpi  36510  heicant  37716  ovoliunnfl  37723  voliunnfl  37725  volsupnfl  37726  mbfresfi  37727  onov0suclim  43392  stoweidlem35  46158  stoweidlem39  46162  prsal  46441  issalnnd  46468  ismeannd  46590  caragenunicl  46647  isomennd  46654  dftpos5  48999  ipolub0  49117