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

Theorem ordeq 4436
Description: Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
Assertion
Ref Expression
ordeq  |-  ( A  =  B  ->  ( Ord  A  <->  Ord  B ) )

Proof of Theorem ordeq
StepHypRef Expression
1 treq 4156 . . 3  |-  ( A  =  B  ->  ( Tr  A  <->  Tr  B )
)
2 weeq2 4419 . . 3  |-  ( A  =  B  ->  (  _E  We  A  <->  _E  We  B ) )
31, 2anbi12d 691 . 2  |-  ( A  =  B  ->  (
( Tr  A  /\  _E  We  A )  <->  ( Tr  B  /\  _E  We  B
) ) )
4 df-ord 4432 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
5 df-ord 4432 . 2  |-  ( Ord 
B  <->  ( Tr  B  /\  _E  We  B ) )
63, 4, 53bitr4g 279 1  |-  ( A  =  B  ->  ( Ord  A  <->  Ord  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1633   Tr wtr 4150    _E cep 4340    We wwe 4388   Ord word 4428
This theorem is referenced by:  elong  4437  limeq  4441  ordelord  4451  ordun  4531  ordeleqon  4617  ordsuc  4642  ordzsl  4673  issmo  6407  issmo2  6408  smoeq  6409  smores  6411  smores2  6413  smodm2  6414  smoiso  6421  tfrlem8  6442  ordtypelem5  7282  ordtypelem7  7284  oicl  7289  oieu  7299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-rex 2583  df-in 3193  df-ss 3200  df-uni 3865  df-tr 4151  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432
  Copyright terms: Public domain W3C validator