This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A = B → Lim ⁡ A ↔ Lim ⁡ B

Proof

Step Hyp Ref Expression
1 ordeq ⊢ A = B → Ord ⁡ A ↔ Ord ⁡ B
2 neeq1 ⊢ A = B → A ≠ ∅ ↔ B ≠ ∅
3 id ⊢ A = B → A = B
4 unieq ⊢ A = B → ⋃ A = ⋃ B
5 3 4 eqeq12d ⊢ A = B → A = ⋃ A ↔ B = ⋃ B
6 1 2 5 3anbi123d ⊢ A = B → Ord ⁡ A ∧ A ≠ ∅ ∧ A = ⋃ A ↔ Ord ⁡ B ∧ B ≠ ∅ ∧ B = ⋃ B
7 df-lim ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ A = ⋃ A
8 df-lim ⊢ Lim ⁡ B ↔ Ord ⁡ B ∧ B ≠ ∅ ∧ B = ⋃ B
9 6 7 8 3bitr4g ⊢ A = B → Lim ⁡ A ↔ Lim ⁡ B