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

Theorem ordeq 4590
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 4310 . . 3  |-  ( A  =  B  ->  ( Tr  A  <->  Tr  B )
)
2 weeq2 4573 . . 3  |-  ( A  =  B  ->  (  _E  We  A  <->  _E  We  B ) )
31, 2anbi12d 693 . 2  |-  ( A  =  B  ->  (
( Tr  A  /\  _E  We  A )  <->  ( Tr  B  /\  _E  We  B
) ) )
4 df-ord 4586 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
5 df-ord 4586 . 2  |-  ( Ord 
B  <->  ( Tr  B  /\  _E  We  B ) )
63, 4, 53bitr4g 281 1  |-  ( A  =  B  ->  ( Ord  A  <->  Ord  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653   Tr wtr 4304    _E cep 4494    We wwe 4542   Ord word 4582
This theorem is referenced by:  elong  4591  limeq  4595  ordelord  4605  ordun  4685  ordeleqon  4771  ordsuc  4796  ordzsl  4827  issmo  6612  issmo2  6613  smoeq  6614  smores  6616  smores2  6618  smodm2  6619  smoiso  6626  tfrlem8  6647  ordtypelem5  7493  ordtypelem7  7495  oicl  7500  oieu  7510
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-in 3329  df-ss 3336  df-uni 4018  df-tr 4305  df-po 4505  df-so 4506  df-fr 4543  df-we 4545  df-ord 4586
  Copyright terms: Public domain W3C validator