Metamath Proof Explorer

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 e. On -> ( A +o 1o ) = ( A u. { A } ) )

Proof

Step Hyp Ref Expression
1 oa1suc 
 |-  ( A e. On -> ( A +o 1o ) = suc A )
2 df-suc 
 |-  suc A = ( A u. { A } )
3 1 2 eqtrdi 
 |-  ( A e. On -> ( A +o 1o ) = ( A u. { A } ) )