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

Theorem ordeq 5445
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 4521 . . 3  |-  ( A  =  B  ->  ( Tr  A  <->  Tr  B )
)
2 weeq2 4838 . . 3  |-  ( A  =  B  ->  (  _E  We  A  <->  _E  We  B ) )
31, 2anbi12d 715 . 2  |-  ( A  =  B  ->  (
( Tr  A  /\  _E  We  A )  <->  ( Tr  B  /\  _E  We  B
) ) )
4 df-ord 5441 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
5 df-ord 5441 . 2  |-  ( Ord 
B  <->  ( Tr  B  /\  _E  We  B ) )
63, 4, 53bitr4g 291 1  |-  ( A  =  B  ->  ( Ord  A  <->  Ord  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   Tr wtr 4515    _E cep 4758    We wwe 4807   Ord word 5437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rex 2781  df-in 3443  df-ss 3450  df-uni 4217  df-tr 4516  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-ord 5441
This theorem is referenced by:  elong  5446  limeq  5450  ordelord  5460  ordun  5539  ordeleqon  6625  ordsuc  6651  ordzsl  6682  issmo  7071  issmo2  7072  smoeq  7073  smores  7075  smores2  7077  smodm2  7078  smoiso  7085  tfrlem8  7106  ordtypelem5  8039  ordtypelem7  8041  oicl  8046  oieu  8056
  Copyright terms: Public domain W3C validator