Theorem uni0 4873

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 5235. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2168. (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 4273	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 487	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1807	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4848	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 324	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4289	1 ⊢ ∪ ∅ = ∅

Syntax hints:   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∅c0 4268  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-nul 4269  df-uni 4846

This theorem is referenced by:  csbuni  4875  uniintsn  4922  iununi  5035  unisn2  5241  eqsnuniex  5297  opswap  6187  unixp0  6241  unixpid  6242  unizlim  6441  iotanul  6472  funfv  6921  dffv2  6929  1stval  7940  2ndval  7941  1stnpr  7942  2ndnpr  7943  1st0  7944  2nd0  7945  1st2val  7966  2nd2val  7967  brtpos0  8180  tpostpos  8193  nnunifi  9198  supval2  9365  sup00  9375  infeq5  9556  rankuni  9785  rankxplim3  9803  iunfictbso  10034  cflim2  10183  fin1a2lem11  10330  itunisuc  10339  itunitc  10341  ttukeylem4  10432  relexpfldd  15010  incexclem  15799  arwval  18008  dprdsn  20011  zrhval  21489  0opn  22894  indistopon  22991  mretopd  23082  hauscmplem  23396  cmpfi  23398  comppfsc  23522  alexsublem  24034  alexsubALTlem2  24038  ptcmplem2  24043  lebnumlem3  24955  old0  27856  made0  27880  locfinref  34032  prsiga  34322  sigapildsys  34353  dya2iocuni  34474  fiunelcarsg  34507  carsgclctunlem1  34508  carsgclctunlem3  34511  fissorduni  35278  fineqvnttrclselem1  35309  wevgblacfn  35344  nnuni  35962  unisnif  36158  limsucncmpi  36680  heicant  38029  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  mbfresfi  38040  onov0suclim  43726  stoweidlem35  46485  stoweidlem39  46489  prsal  46768  issalnnd  46795  ismeannd  46917  caragenunicl  46974  isomennd  46981  dftpos5  49371  ipolub0  49489