Theorem limeq

Description: Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	limeq	⊢ ( 𝐴 = 𝐵 → ( Lim 𝐴 ↔ Lim 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ordeq	⊢ ( 𝐴 = 𝐵 → ( Ord 𝐴 ↔ Ord 𝐵 ) )
2		neeq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
3		id	⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
4		unieq	⊢ ( 𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵 )
5	3 4	eqeq12d	⊢ ( 𝐴 = 𝐵 → ( 𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵 ) )
6	1 2 5	3anbi123d	⊢ ( 𝐴 = 𝐵 → ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) ↔ ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵 ) ) )
7		df-lim	⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) )
8		df-lim	⊢ ( Lim 𝐵 ↔ ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵 ) )
9	6 7 8	3bitr4g	⊢ ( 𝐴 = 𝐵 → ( Lim 𝐴 ↔ Lim 𝐵 ) )