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

Theorem ordeq 6381
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 5277 . . 3 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
2 weeq2 5671 . . 3 (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵))
31, 2anbi12d 630 . 2 (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵)))
4 df-ord 6377 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
5 df-ord 6377 . 2 (Ord 𝐵 ↔ (Tr 𝐵 ∧ E We 𝐵))
63, 4, 53bitr4g 313 1 (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  Tr wtr 5269   E cep 5585   We wwe 5636  Ord word 6373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-v 3475  df-in 3956  df-ss 3966  df-uni 4913  df-tr 5270  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-ord 6377
This theorem is referenced by:  elong  6382  limeq  6386  ordelord  6396  ordun  6478  ordeleqon  7790  ordsuc  7822  ordsucOLD  7823  ordzsl  7855  issmo  8375  issmo2  8376  smoeq  8377  smores  8379  smores2  8381  smodm2  8382  smoiso  8389  tfrlem8  8411  ord3  8510  ordtypelem5  9553  ordtypelem7  9555  oicl  9560  oieu  9570  dfsucon  42984
  Copyright terms: Public domain W3C validator