Metamath Proof Explorer

Theorem nordeq

Description: A member of an ordinal class is not equal to it. (Contributed by NM, 25-May-1998)

Ref Expression
Assertion nordeq 
|- ( ( Ord A /\ B e. A ) -> A =/= B )

Proof

Step Hyp Ref Expression
1 ordirr 
 |-  ( Ord A -> -. A e. A )
2 eleq1 
 |-  ( A = B -> ( A e. A <-> B e. A ) )
3 2 notbid 
 |-  ( A = B -> ( -. A e. A <-> -. B e. A ) )
4 1 3 syl5ibcom 
 |-  ( Ord A -> ( A = B -> -. B e. A ) )
5 4 necon2ad 
 |-  ( Ord A -> ( B e. A -> A =/= B ) )
6 5 imp 
 |-  ( ( Ord A /\ B e. A ) -> A =/= B )