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

Theorem ordeq 4874
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 4538 . . 3  |-  ( A  =  B  ->  ( Tr  A  <->  Tr  B )
)
2 weeq2 4857 . . 3  |-  ( A  =  B  ->  (  _E  We  A  <->  _E  We  B ) )
31, 2anbi12d 708 . 2  |-  ( A  =  B  ->  (
( Tr  A  /\  _E  We  A )  <->  ( Tr  B  /\  _E  We  B
) ) )
4 df-ord 4870 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
5 df-ord 4870 . 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 367    = wceq 1398   Tr wtr 4532    _E cep 4778    We wwe 4826   Ord word 4866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-in 3468  df-ss 3475  df-uni 4236  df-tr 4533  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870
This theorem is referenced by:  elong  4875  limeq  4879  ordelord  4889  ordun  4968  ordeleqon  6597  ordsuc  6622  ordzsl  6653  issmo  7011  issmo2  7012  smoeq  7013  smores  7015  smores2  7017  smodm2  7018  smoiso  7025  tfrlem8  7045  ordtypelem5  7939  ordtypelem7  7941  oicl  7946  oieu  7956
  Copyright terms: Public domain W3C validator