Metamath Proof Explorer

Theorem oa0

Description: Addition with zero. Proposition 8.3 of TakeutiZaring p. 57. Definition 2.3 of Schloeder p. 4. (Contributed by NM, 3-May-1995) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	oa0	$⊢ A \in On \to A +_{𝑜} \emptyset = A$

Proof

Step	Hyp	Ref	Expression
1		0elon	$⊢ \emptyset \in On$
2		oav	$⊢ (A \in On \land \emptyset \in On) \to A +_{𝑜} \emptyset = rec ((x \in V ⟼ suc x), A) (\emptyset)$
3	1 2	mpan2	$⊢ A \in On \to A +_{𝑜} \emptyset = rec ((x \in V ⟼ suc x), A) (\emptyset)$
4		rdg0g	$⊢ A \in On \to rec ((x \in V ⟼ suc x), A) (\emptyset) = A$
5	3 4	eqtrd	$⊢ A \in On \to A +_{𝑜} \emptyset = A$