Theorem limuni 4943

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

Assertion

Ref	Expression
limuni

Proof of Theorem limuni

Step	Hyp	Ref	Expression
1		df-lim 4888	. 2
2	1	simp3bi 1013	1

Syntax hints:  ->wi 4  =wceq 1395  =/=wne 2652  c0 3784  U.cuni 4249  Ordword 4882  Limwlim 4884

This theorem is referenced by:  limuni2  4944  unizlim  4999  nlimsucg  6677  oa0r  7207  om1r  7211  oarec  7230  oeworde  7261  oeeulem  7269  infeq5i  8074  r1sdom  8213  rankxplim3  8320  cflm  8651  coflim  8662  cflim2  8664  cfss  8666  cfslbn  8668  limsucncmpi  29910

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 185  df-an 371  df-3an 975  df-lim 4888