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 5263. (Revised by Eric Schmidt, 4-Apr-2007.) Avoid ax-11 2197. (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 4286	. . . . 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 2147  ∅c0 4281  ∪ 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-nul 4282  df-uni 4871

This theorem is used by:  csbuni  4901  uniintsn  4948  iununi  5062  unisn2  5269  eqsnuniex  5327  opswap  6243  unixp0  6304  unixpid  6305  unizlim  6505  iotanul  6537  funfv  6995  dffv2  7003  1stval  8027  2ndval  8028  1stnpr  8029  2ndnpr  8030  1st0  8031  2nd0  8032  1st2val  8053  2nd2val  8054  brtpos0  8278  tpostpos  8291  fissorduni  9310  nnunifi  9311  supval2  9474  sup00  9484  infeq5  9665  rankuni  9906  rankxplim3  9925  iunfictbso  10220  cflim2  10368  fin1a2lem11  10515  itunisuc  10524  itunitc  10526  ttukeylem4  10617  relexpfldd  15232  incexclem  16034  arwval  18247  dprdsn  20282  zrhval  21843  0opn  23252  indistopon  23349  mretopd  23440  hauscmplem  23754  cmpfi  23756  comppfsc  23881  alexsublem  24393  alexsubALTlem2  24397  ptcmplem2  24402  lebnumlem3  25314  old0  28255  made0  28279  locfinref  34543  prsiga  34833  sigapildsys  34865  dya2iocuni  34985  fiunelcarsg  35018  carsgclctunlem1  35019  carsgclctunlem3  35022  fineqvnttrclselem1  35889  wevgblacfn  36039  nnuni  36670  unisnif  36865  limsucncmpi  37411  heicant  38765  ovoliunnfl  38772  voliunnfl  38774  volsupnfl  38775  mbfresfi  38776  onov0suclim  44468  stoweidlem35  47250  stoweidlem39  47254  prsal  47533  issalnnd  47560  ismeannd  47682  caragenunicl  47739  isomennd  47746  dftpos5  50192  ipolub0  50311