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ωA+𝑜=A

Proof

Step Hyp Ref Expression
1 nnon AωAOn
2 oa0 AOnA+𝑜=A
3 1 2 syl AωA+𝑜=A