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 4284	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 492	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1833	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4870	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4302	1 ⊢ ∪ ∅ = ∅

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∅c0 4279  ∪ cuni 4867

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-nul 4280  df-uni 4868

This theorem is used by:  csbuni  4898  uniintsn  4945  iununi  5059  unisn2  5266  eqsnuniex  5323  opswap  6223  unixp0  6279  unixpid  6280  unizlim  6480  iotanul  6511  funfv  6964  dffv2  6972  1stval  7992  2ndval  7993  1stnpr  7994  2ndnpr  7995  1st0  7996  2nd0  7997  1st2val  8018  2nd2val  8019  brtpos0  8234  tpostpos  8247  fissorduni  9266  nnunifi  9267  supval2  9431  sup00  9441  infeq5  9622  rankuni  9860  rankxplim3  9879  iunfictbso  10174  cflim2  10322  fin1a2lem11  10469  itunisuc  10478  itunitc  10480  ttukeylem4  10571  relexpfldd  15183  incexclem  15985  arwval  18198  dprdsn  20232  zrhval  21793  0opn  23202  indistopon  23299  mretopd  23390  hauscmplem  23704  cmpfi  23706  comppfsc  23831  alexsublem  24343  alexsubALTlem2  24347  ptcmplem2  24352  lebnumlem3  25264  old0  28207  made0  28231  locfinref  34455  prsiga  34745  sigapildsys  34777  dya2iocuni  34898  fiunelcarsg  34931  carsgclctunlem1  34932  carsgclctunlem3  34935  fineqvnttrclselem1  35762  wevgblacfn  35863  nnuni  36461  unisnif  36657  limsucncmpi  37203  heicant  38541  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  mbfresfi  38552  onov0suclim  44234  stoweidlem35  46989  stoweidlem39  46993  prsal  47272  issalnnd  47299  ismeannd  47421  caragenunicl  47478  isomennd  47485  dftpos5  49926  ipolub0  50044