Theorem limuni 6219

Description: A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)

Assertion

Ref	Expression
limuni	⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Proof of Theorem limuni

Step	Hyp	Ref	Expression
1		df-lim 6164	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
2	1	simp3bi 1144	1 ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Syntax hints:   → wi 4   = wceq 1538   ≠ wne 2987  ∅c0 4243  ∪ cuni 4800  Ord word 6158  Lim wlim 6160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-lim 6164

This theorem is referenced by:  limuni2  6220  unizlim  6275  nlimsucg  7537  oa0r  8146  om1r  8152  oarec  8171  oeworde  8202  oeeulem  8210  infeq5i  9083  r1sdom  9187  rankxplim3  9294  cflm  9661  coflim  9672  cflim2  9674  cfss  9676  cfslbn  9678  limsucncmpi  33906  dfom6  40239