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

Theorem ordeq 5694
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 4723 . . 3 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
2 weeq2 5068 . . 3 (𝐴 = 𝐵 → ( E We 𝐴 ↔ E We 𝐵))
31, 2anbi12d 746 . 2 (𝐴 = 𝐵 → ((Tr 𝐴 ∧ E We 𝐴) ↔ (Tr 𝐵 ∧ E We 𝐵)))
4 df-ord 5690 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
5 df-ord 5690 . 2 (Ord 𝐵 ↔ (Tr 𝐵 ∧ E We 𝐵))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  Tr wtr 4717   E cep 4988   We wwe 5037  Ord word 5686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-in 3566  df-ss 3573  df-uni 4408  df-tr 4718  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-ord 5690
This theorem is referenced by:  elong  5695  limeq  5699  ordelord  5709  ordun  5793  ordeleqon  6942  ordsuc  6968  ordzsl  6999  issmo  7397  issmo2  7398  smoeq  7399  smores  7401  smores2  7403  smodm2  7404  smoiso  7411  tfrlem8  7432  ordtypelem5  8379  ordtypelem7  8381  oicl  8386  oieu  8396
  Copyright terms: Public domain W3C validator