Theorem uni0 4902

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 5270. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2192. (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 4292	. . . . 5 ⊢ ¬ 𝑦 ∈ ∅
2	1	intnan 491	. . . 4 ⊢ ¬ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
3	2	nex 1830	. . 3 ⊢ ¬ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅)
4		eluni 4876	. . 3 ⊢ (𝑥 ∈ ∪ ∅ ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅))
5	3, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0 4310	1 ⊢ ∪ ∅ = ∅

Syntax hints:   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∅c0 4287  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-nul 4288  df-uni 4874

This theorem is referenced by:  csbuni  4904  uniintsn  4951  iununi  5066  unisn2  5276  eqsnuniex  5334  opswap  6232  unixp0  6286  unixpid  6287  unizlim  6487  iotanul  6518  funfv  6970  dffv2  6978  1stval  7989  2ndval  7990  1stnpr  7991  2ndnpr  7992  1st0  7993  2nd0  7994  1st2val  8015  2nd2val  8016  brtpos0  8230  tpostpos  8243  nnunifi  9252  supval2  9416  sup00  9426  infeq5  9607  rankuni  9836  rankxplim3  9854  iunfictbso  10099  cflim2  10248  fin1a2lem11  10395  itunisuc  10404  itunitc  10406  ttukeylem4  10497  relexpfldd  15089  incexclem  15892  arwval  18101  dprdsn  20109  zrhval  21638  0opn  23042  indistopon  23139  mretopd  23230  hauscmplem  23544  cmpfi  23546  comppfsc  23670  alexsublem  24182  alexsubALTlem2  24186  ptcmplem2  24191  lebnumlem3  25103  old0  28010  made0  28034  locfinref  34209  prsiga  34499  sigapildsys  34530  dya2iocuni  34651  fiunelcarsg  34684  carsgclctunlem1  34685  carsgclctunlem3  34688  fissorduni  35458  fineqvnttrclselem1  35512  wevgblacfn  35573  nnuni  36197  unisnif  36393  limsucncmpi  36934  heicant  38284  ovoliunnfl  38291  voliunnfl  38293  volsupnfl  38294  mbfresfi  38295  onov0suclim  43981  stoweidlem35  46729  stoweidlem39  46733  prsal  47012  issalnnd  47039  ismeannd  47161  caragenunicl  47218  isomennd  47225  dftpos5  49629  ipolub0  49747