Metamath Proof Explorer

Theorem ordeq

Description: Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993)

Ref Expression
Assertion ordeq 
|- ( A = B -> ( Ord A <-> Ord B ) )

Proof

Step Hyp Ref Expression
1 treq 
 |-  ( A = B -> ( Tr A <-> Tr B ) )
2 weeq2 
 |-  ( A = B -> ( _E We A <-> _E We B ) )
3 1 2 anbi12d 
 |-  ( A = B -> ( ( Tr A /\ _E We A ) <-> ( Tr B /\ _E We B ) ) )
4 df-ord 
 |-  ( Ord A <-> ( Tr A /\ _E We A ) )
5 df-ord 
 |-  ( Ord B <-> ( Tr B /\ _E We B ) )
6 3 4 5 3bitr4g 
 |-  ( A = B -> ( Ord A <-> Ord B ) )