Metamath Proof Explorer


Theorem nna0

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 )

Proof

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 )