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	⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) = ( 𝐴 ∪ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		oa1suc	⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) = suc 𝐴 )
2		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
3	1 2	eqtrdi	⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) = ( 𝐴 ∪ { 𝐴 } ) )