Description: A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | elnn | |- ( ( A e. B /\ B e. _om ) -> A e. _om ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordom | |- Ord _om |
|
2 | ordtr | |- ( Ord _om -> Tr _om ) |
|
3 | trel | |- ( Tr _om -> ( ( A e. B /\ B e. _om ) -> A e. _om ) ) |
|
4 | 1 2 3 | mp2b | |- ( ( A e. B /\ B e. _om ) -> A e. _om ) |