Theorem oa1un

Description: Given A e. On , let A +o 1o be defined to be the union of A and { A } . Compare with oa1suc . (Contributed by RP, 27-Sep-2023)

	Ref	Expression
Assertion	oa1un	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}{1}_{𝑜}=A\cup \left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		oa1suc	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}A$$
2		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
3	1 2	eqtrdi	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}{1}_{𝑜}=A\cup \left\{A\right\}$$