Theorem limuni 5702

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 5645	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
2	1	simp3bi 1071	1 ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780  ∅c0 3874  ∪ cuni 4372  Ord word 5639  Lim wlim 5641

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 196  df-an 385  df-3an 1033  df-lim 5645

This theorem is referenced by:  limuni2  5703  unizlim  5761  nlimsucg  6934  oa0r  7505  om1r  7510  oarec  7529  oeworde  7560  oeeulem  7568  infeq5i  8416  r1sdom  8520  rankxplim3  8627  cflm  8955  coflim  8966  cflim2  8968  cfss  8970  cfslbn  8972  limsucncmpi  31614