![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ordeq | Structured version Visualization version GIF version |
Description: Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.) |
Ref | Expression |
---|---|
ordeq | ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | treq 5274 | . . 3 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) | |
2 | weeq2 5666 | . . 3 ⊢ (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵)) | |
3 | 1, 2 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵))) |
4 | df-ord 6368 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
5 | df-ord 6368 | . 2 ⊢ (Ord 𝐵 ↔ (Tr 𝐵 ∧ E We 𝐵)) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 Tr wtr 5266 E cep 5580 We wwe 5631 Ord word 6364 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-v 3477 df-in 3956 df-ss 3966 df-uni 4910 df-tr 5267 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-ord 6368 |
This theorem is referenced by: elong 6373 limeq 6377 ordelord 6387 ordun 6469 ordeleqon 7769 ordsuc 7801 ordsucOLD 7802 ordzsl 7834 issmo 8348 issmo2 8349 smoeq 8350 smores 8352 smores2 8354 smodm2 8355 smoiso 8362 tfrlem8 8384 ord3 8483 ordtypelem5 9517 ordtypelem7 9519 oicl 9524 oieu 9534 dfsucon 42274 |
Copyright terms: Public domain | W3C validator |