MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordeq Structured version   Visualization version   GIF version

Theorem ordeq 6372
Description: Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
Assertion
Ref Expression
ordeq (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))

Proof of Theorem ordeq
StepHypRef Expression
1 treq 5274 . . 3 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
2 weeq2 5666 . . 3 (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵))
31, 2anbi12d 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 𝐵))
63, 4, 53bitr4g 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