Theorem uni0 4899

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905  df-nul 4283  df-uni 4871

This theorem is used by:  csbuni  4901  uniintsn  4948  iununi  5063  unisn2  5273  eqsnuniex  5330  opswap  6229  unixp0  6285  unixpid  6286  unizlim  6486  iotanul  6517  funfv  6969  dffv2  6977  1stval  7992  2ndval  7993  1stnpr  7994  2ndnpr  7995  1st0  7996  2nd0  7997  1st2val  8018  2nd2val  8019  brtpos0  8235  tpostpos  8248  nnunifi  9265  supval2  9429  sup00  9439  infeq5  9620  rankuni  9849  rankxplim3  9867  iunfictbso  10121  cflim2  10269  fin1a2lem11  10416  itunisuc  10425  itunitc  10427  ttukeylem4  10518  relexpfldd  15127  incexclem  15929  arwval  18138  dprdsn  20171  zrhval  21726  0opn  23135  indistopon  23232  mretopd  23323  hauscmplem  23637  cmpfi  23639  comppfsc  23764  alexsublem  24276  alexsubALTlem2  24280  ptcmplem2  24285  lebnumlem3  25197  old0  28112  made0  28136  locfinref  34359  prsiga  34649  sigapildsys  34681  dya2iocuni  34802  fiunelcarsg  34835  carsgclctunlem1  34836  carsgclctunlem3  34839  fissorduni  35602  fineqvnttrclselem1  35655  wevgblacfn  35716  nnuni  36314  unisnif  36510  limsucncmpi  37072  heicant  38412  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  mbfresfi  38423  onov0suclim  44123  stoweidlem35  46871  stoweidlem39  46875  prsal  47154  issalnnd  47181  ismeannd  47303  caragenunicl  47360  isomennd  47367  dftpos5  49808  ipolub0  49926