Theorem uni0 4897

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 5261. (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 4293	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 491	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1823	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4871	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4310	1 ⊢ ∪ ∅ = ∅

Syntax hints:   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∅c0 4288  ∪ cuni 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3910  df-nul 4289  df-uni 4869

This theorem is referenced by:  csbuni  4899  uniintsn  4946  iununi  5061  unisn2  5267  eqsnuniex  5323  opswap  6220  unixp0  6274  unixpid  6275  unizlim  6474  iotanul  6505  funfv  6958  dffv2  6966  1stval  7976  2ndval  7977  1stnpr  7978  2ndnpr  7979  1st0  7980  2nd0  7981  1st2val  8002  2nd2val  8003  brtpos0  8217  tpostpos  8230  nnunifi  9239  supval2  9403  sup00  9413  infeq5  9594  rankuni  9823  rankxplim3  9841  iunfictbso  10086  cflim2  10235  fin1a2lem11  10382  itunisuc  10391  itunitc  10393  ttukeylem4  10484  relexpfldd  15077  incexclem  15880  arwval  18090  dprdsn  20099  zrhval  21617  0opn  23022  indistopon  23119  mretopd  23210  hauscmplem  23524  cmpfi  23526  comppfsc  23650  alexsublem  24162  alexsubALTlem2  24166  ptcmplem2  24171  lebnumlem3  25083  old0  27990  made0  28014  locfinref  34148  prsiga  34438  sigapildsys  34469  dya2iocuni  34590  fiunelcarsg  34623  carsgclctunlem1  34624  carsgclctunlem3  34627  fissorduni  35395  fineqvnttrclselem1  35429  wevgblacfn  35466  nnuni  36090  unisnif  36286  limsucncmpi  36818  heicant  38166  ovoliunnfl  38173  voliunnfl  38175  volsupnfl  38176  mbfresfi  38177  onov0suclim  43863  stoweidlem35  46607  stoweidlem39  46611  prsal  46890  issalnnd  46917  ismeannd  47039  caragenunicl  47096  isomennd  47103  dftpos5  49503  ipolub0  49621