Theorem dflim2 4160

Description: Alias for df-ilim 4159. Use it instead of df-ilim 4159 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)

Assertion

Ref	Expression
dflim2	⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))

Proof of Theorem dflim2

Step	Hyp	Ref	Expression
1		df-ilim 4159	1 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))

Syntax hints:   ↔ wb 103   ∧ w3a 920   = wceq 1285   ∈ wcel 1434  ∅c0 3269  ∪ cuni 3627  Ord word 4152  Lim wlim 4154

This theorem depends on definitions:  df-ilim 4159

This theorem is referenced by:  limeq  4167  nlim0  4184  limord  4185  limuni  4186  0ellim  4188  limon  4292  limom  4390