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

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

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 3444  df-dif 3906  df-nul 4288  df-uni 4866

This theorem is referenced by:  csbuni  4895  uniintsn  4942  iununi  5056  unisn2  5259  eqsnuniex  5308  opswap  6195  unixp0  6249  unixpid  6250  unizlim  6449  iotanul  6480  funfv  6929  dffv2  6937  1stval  7945  2ndval  7946  1stnpr  7947  2ndnpr  7948  1st0  7949  2nd0  7950  1st2val  7971  2nd2val  7972  brtpos0  8185  tpostpos  8198  nnunifi  9203  supval2  9370  sup00  9380  infeq5  9558  rankuni  9787  rankxplim3  9805  iunfictbso  10036  cflim2  10185  fin1a2lem11  10332  itunisuc  10341  itunitc  10343  ttukeylem4  10434  relexpfldd  14985  incexclem  15771  arwval  17979  dprdsn  19979  zrhval  21474  0opn  22860  indistopon  22957  mretopd  23048  hauscmplem  23362  cmpfi  23364  comppfsc  23488  alexsublem  24000  alexsubALTlem2  24004  ptcmplem2  24009  lebnumlem3  24930  old0  27847  made0  27871  locfinref  34018  prsiga  34308  sigapildsys  34339  dya2iocuni  34460  fiunelcarsg  34493  carsgclctunlem1  34494  carsgclctunlem3  34497  fissorduni  35265  fineqvnttrclselem1  35296  wevgblacfn  35322  nnuni  35940  unisnif  36136  limsucncmpi  36658  heicant  37900  ovoliunnfl  37907  voliunnfl  37909  volsupnfl  37910  mbfresfi  37911  onov0suclim  43625  stoweidlem35  46387  stoweidlem39  46391  prsal  46670  issalnnd  46697  ismeannd  46819  caragenunicl  46876  isomennd  46883  dftpos5  49227  ipolub0  49345