| 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 5267 | . . 3 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) | |
| 2 | weeq2 5673 | . . 3 ⊢ (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵)) | |
| 3 | 1, 2 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵))) |
| 4 | df-ord 6387 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | |
| 5 | df-ord 6387 | . 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 206 ∧ wa 395 = wceq 1540 Tr wtr 5259 E cep 5583 We wwe 5636 Ord word 6383 |
| 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-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 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 |
| This theorem is referenced by: elong 6392 limeq 6396 ordelord 6406 ordun 6488 ordeleqon 7802 ordsuc 7833 ordsucOLD 7834 ordzsl 7866 issmo 8388 issmo2 8389 smoeq 8390 smores 8392 smores2 8394 smodm2 8395 smoiso 8402 tfrlem8 8424 ord3 8523 ordtypelem5 9562 ordtypelem7 9564 oicl 9569 oieu 9579 dfsucon 43536 |
| Copyright terms: Public domain | W3C validator |