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 ) |
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 ) |