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 5142 | . . 3 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) | |
2 | weeq2 5514 | . . 3 ⊢ (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵)) | |
3 | 1, 2 | anbi12d 634 | . 2 ⊢ (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵))) |
4 | df-ord 6175 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
5 | df-ord 6175 | . 2 ⊢ (Ord 𝐵 ↔ (Tr 𝐵 ∧ E We 𝐵)) | |
6 | 3, 4, 5 | 3bitr4g 317 | 1 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 Tr wtr 5136 E cep 5433 We wwe 5482 Ord word 6171 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-v 3400 df-in 3850 df-ss 3860 df-uni 4797 df-tr 5137 df-po 5442 df-so 5443 df-fr 5483 df-we 5485 df-ord 6175 |
This theorem is referenced by: elong 6180 limeq 6184 ordelord 6194 ordun 6273 ordeleqon 7522 ordsuc 7548 ordzsl 7579 issmo 8014 issmo2 8015 smoeq 8016 smores 8018 smores2 8020 smodm2 8021 smoiso 8028 tfrlem8 8049 ordtypelem5 9059 ordtypelem7 9061 oicl 9066 oieu 9076 dfsucon 40684 |
Copyright terms: Public domain | W3C validator |