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 5197 | . . 3 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) | |
2 | weeq2 5578 | . . 3 ⊢ (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵)) | |
3 | 1, 2 | anbi12d 631 | . 2 ⊢ (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵))) |
4 | df-ord 6269 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
5 | df-ord 6269 | . 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 396 = wceq 1539 Tr wtr 5191 E cep 5494 We wwe 5543 Ord word 6265 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-v 3434 df-in 3894 df-ss 3904 df-uni 4840 df-tr 5192 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-ord 6269 |
This theorem is referenced by: elong 6274 limeq 6278 ordelord 6288 ordun 6367 ordeleqon 7632 ordsuc 7661 ordzsl 7692 issmo 8179 issmo2 8180 smoeq 8181 smores 8183 smores2 8185 smodm2 8186 smoiso 8193 tfrlem8 8215 ordtypelem5 9281 ordtypelem7 9283 oicl 9288 oieu 9298 dfsucon 41130 |
Copyright terms: Public domain | W3C validator |