Theorem nmull0

Description: Natural multiplication by zero. (Contributed by Scott Fenton, 10-Jun-2026)

	Ref	Expression
Assertion	nmull0	⊢ ( 𝐴 ∈ On → ( ∅ ·no 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		0elon	⊢ ∅ ∈ On
2		nmulcom	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ On ) → ( 𝐴 ·no ∅ ) = ( ∅ ·no 𝐴 ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 ·no ∅ ) = ( ∅ ·no 𝐴 ) )
4		nmulr0	⊢ ( 𝐴 ∈ On → ( 𝐴 ·no ∅ ) = ∅ )
5	3 4	eqtr3d	⊢ ( 𝐴 ∈ On → ( ∅ ·no 𝐴 ) = ∅ )