Theorem uni0 4895

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 5259. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2193. (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 4283	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 492	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1832	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4869	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4301	1 ⊢ ∪ ∅ = ∅

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∅c0 4278  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047  df-nul 4279  df-uni 4867

This theorem is used by:  csbuni  4897  uniintsn  4944  iununi  5058  unisn2  5265  eqsnuniex  5322  opswap  6230  unixp0  6286  unixpid  6287  unizlim  6487  iotanul  6518  funfv  6972  dffv2  6980  1stval  8003  2ndval  8004  1stnpr  8005  2ndnpr  8006  1st0  8007  2nd0  8008  1st2val  8029  2nd2val  8030  brtpos0  8253  tpostpos  8266  fissorduni  9285  nnunifi  9286  supval2  9450  sup00  9460  infeq5  9641  rankuni  9882  rankxplim3  9901  iunfictbso  10196  cflim2  10344  fin1a2lem11  10491  itunisuc  10500  itunitc  10502  ttukeylem4  10593  relexpfldd  15208  incexclem  16010  arwval  18223  dprdsn  20257  zrhval  21818  0opn  23227  indistopon  23324  mretopd  23415  hauscmplem  23729  cmpfi  23731  comppfsc  23856  alexsublem  24368  alexsubALTlem2  24372  ptcmplem2  24377  lebnumlem3  25289  old0  28230  made0  28254  locfinref  34519  prsiga  34809  sigapildsys  34841  dya2iocuni  34961  fiunelcarsg  34994  carsgclctunlem1  34995  carsgclctunlem3  34998  fineqvnttrclselem1  35845  wevgblacfn  35958  nnuni  36584  unisnif  36779  limsucncmpi  37325  heicant  38666  ovoliunnfl  38673  voliunnfl  38675  volsupnfl  38676  mbfresfi  38677  onov0suclim  44369  stoweidlem35  47138  stoweidlem39  47142  prsal  47421  issalnnd  47448  ismeannd  47570  caragenunicl  47627  isomennd  47634  dftpos5  50080  ipolub0  50199