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

Theorem ordeq 4891
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 4552 . . 3  |-  ( A  =  B  ->  ( Tr  A  <->  Tr  B )
)
2 weeq2 4874 . . 3  |-  ( A  =  B  ->  (  _E  We  A  <->  _E  We  B ) )
31, 2anbi12d 710 . 2  |-  ( A  =  B  ->  (
( Tr  A  /\  _E  We  A )  <->  ( Tr  B  /\  _E  We  B
) ) )
4 df-ord 4887 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
5 df-ord 4887 . 2  |-  ( Ord 
B  <->  ( Tr  B  /\  _E  We  B ) )
63, 4, 53bitr4g 288 1  |-  ( A  =  B  ->  ( Ord  A  <->  Ord  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   Tr wtr 4546    _E cep 4795    We wwe 4843   Ord word 4883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-rex 2823  df-in 3488  df-ss 3495  df-uni 4252  df-tr 4547  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887
This theorem is referenced by:  elong  4892  limeq  4896  ordelord  4906  ordun  4985  ordeleqon  6619  ordsuc  6644  ordzsl  6675  issmo  7031  issmo2  7032  smoeq  7033  smores  7035  smores2  7037  smodm2  7038  smoiso  7045  tfrlem8  7065  ordtypelem5  7959  ordtypelem7  7961  oicl  7966  oieu  7976
  Copyright terms: Public domain W3C validator