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

Theorem ordeq 6391
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 5267 . . 3 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
2 weeq2 5673 . . 3 (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵))
31, 2anbi12d 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 𝐵))
63, 4, 53bitr4g 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