Metamath Proof Explorer

Theorem nnm0

Description: Multiplication with zero. Theorem 4J(A1) of Enderton p. 80. (Contributed by NM, 20-Sep-1995)

Ref Expression
Assertion nnm0 
|- ( A e. _om -> ( A .o (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( A e. _om -> A e. On )
2 om0 
 |-  ( A e. On -> ( A .o (/) ) = (/) )
3 1 2 syl 
 |-  ( A e. _om -> ( A .o (/) ) = (/) )