| 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 6391 | . . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) | |
| 2 | neeq1 3003 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅)) | |
| 3 | id 22 | . . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
| 4 | unieq 4918 | . . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
| 5 | 3, 4 | eqeq12d 2753 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵)) |
| 6 | 1, 2, 5 | 3anbi123d 1438 | . 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))) |
| 7 | df-lim 6389 | . 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
| 8 | df-lim 6389 | . 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)) | |
| 9 | 6, 7, 8 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1087 = wceq 1540 ≠ wne 2940 ∅c0 4333 ∪ cuni 4907 Ord word 6383 Lim wlim 6385 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-v 3482 df-ss 3968 df-uni 4908 df-tr 5260 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-ord 6387 df-lim 6389 |
| This theorem is referenced by: limuni2 6446 0ellim 6447 limuni3 7873 tfinds2 7885 dfom2 7889 limomss 7892 nnlim 7901 limom 7903 ssnlim 7907 onfununi 8381 tfr1a 8434 tz7.44lem1 8445 tz7.44-2 8447 tz7.44-3 8448 1ellim 8536 2ellim 8537 oeeulem 8639 limensuc 9194 elom3 9688 r1funlim 9806 rankxplim2 9920 rankxplim3 9921 rankxpsuc 9922 infxpenlem 10053 alephislim 10123 cflim2 10303 winalim 10735 rankcf 10817 gruina 10858 scutbdaybnd2lim 27862 rdgprc0 35794 dfrdg2 35796 dfrdg4 35952 limsucncmpi 36446 limsucncmp 36447 omlimcl2 43254 onexlimgt 43255 onov0suclim 43287 succlg 43341 dflim5 43342 nlim1NEW 43455 nlim2NEW 43456 nlim3 43457 nlim4 43458 dfsucon 43536 |
| Copyright terms: Public domain | W3C validator |