Theorem uni0 4906

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 5274. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2195. (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 4294	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 492	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1833	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4880	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4312	1 ⊢ ∪ ∅ = ∅

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∅c0 4289  ∪ cuni 4877

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-dif 3911  df-nul 4290  df-uni 4878

This theorem is used by:  csbuni  4908  uniintsn  4955  iununi  5070  unisn2  5280  eqsnuniex  5337  opswap  6235  unixp0  6291  unixpid  6292  unizlim  6492  iotanul  6523  funfv  6975  dffv2  6983  1stval  7997  2ndval  7998  1stnpr  7999  2ndnpr  8000  1st0  8001  2nd0  8002  1st2val  8023  2nd2val  8024  brtpos0  8238  tpostpos  8251  nnunifi  9261  supval2  9425  sup00  9435  infeq5  9616  rankuni  9845  rankxplim3  9863  iunfictbso  10117  cflim2  10265  fin1a2lem11  10412  itunisuc  10421  itunitc  10423  ttukeylem4  10514  relexpfldd  15113  incexclem  15916  arwval  18125  dprdsn  20139  zrhval  21694  0opn  23098  indistopon  23195  mretopd  23286  hauscmplem  23600  cmpfi  23602  comppfsc  23726  alexsublem  24238  alexsubALTlem2  24242  ptcmplem2  24247  lebnumlem3  25159  old0  28069  made0  28093  locfinref  34262  prsiga  34552  sigapildsys  34583  dya2iocuni  34704  fiunelcarsg  34737  carsgclctunlem1  34738  carsgclctunlem3  34741  fissorduni  35504  fineqvnttrclselem1  35557  wevgblacfn  35618  nnuni  36239  unisnif  36435  limsucncmpi  36996  heicant  38346  ovoliunnfl  38353  voliunnfl  38355  volsupnfl  38356  mbfresfi  38357  onov0suclim  44041  stoweidlem35  46789  stoweidlem39  46793  prsal  47072  issalnnd  47099  ismeannd  47221  caragenunicl  47278  isomennd  47285  dftpos5  49692  ipolub0  49810