Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > limeq | Structured version Visualization version GIF version |
Description: Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
limeq | ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordeq 6193 | . . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) | |
2 | neeq1 3078 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅)) | |
3 | id 22 | . . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
4 | unieq 4840 | . . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
5 | 3, 4 | eqeq12d 2837 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵)) |
6 | 1, 2, 5 | 3anbi123d 1432 | . 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))) |
7 | df-lim 6191 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
8 | df-lim 6191 | . 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)) | |
9 | 6, 7, 8 | 3bitr4g 316 | 1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ w3a 1083 = wceq 1533 ≠ wne 3016 ∅c0 4291 ∪ cuni 4832 Ord word 6185 Lim wlim 6187 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-ne 3017 df-ral 3143 df-rex 3144 df-in 3943 df-ss 3952 df-uni 4833 df-tr 5166 df-po 5469 df-so 5470 df-fr 5509 df-we 5511 df-ord 6189 df-lim 6191 |
This theorem is referenced by: limuni2 6247 0ellim 6248 limuni3 7561 tfinds2 7572 dfom2 7576 limomss 7579 nnlim 7587 limom 7589 ssnlim 7593 onfununi 7972 tfr1a 8024 tz7.44lem1 8035 tz7.44-2 8037 tz7.44-3 8038 oeeulem 8221 limensuc 8688 elom3 9105 r1funlim 9189 rankxplim2 9303 rankxplim3 9304 rankxpsuc 9305 infxpenlem 9433 alephislim 9503 cflim2 9679 winalim 10111 rankcf 10193 gruina 10234 rdgprc0 33033 dfrdg2 33035 dfrdg4 33407 limsucncmpi 33788 limsucncmp 33789 dfsucon 39882 |
Copyright terms: Public domain | W3C validator |