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 )