Description: Addition with zero. Theorem 4I(A1) of Enderton p. 79. (Contributed by NM, 20-Sep-1995)
Ref | Expression | ||
---|---|---|---|
Assertion | nna0 | |- ( A e. _om -> ( A +o (/) ) = A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnon | |- ( A e. _om -> A e. On ) |
|
2 | oa0 | |- ( A e. On -> ( A +o (/) ) = A ) |
|
3 | 1 2 | syl | |- ( A e. _om -> ( A +o (/) ) = A ) |