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 )