Metamath Proof Explorer

Theorem oldsuc

Description: The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion oldsuc 
|- ( A e. On -> ( _Old ` suc A ) = ( ( _Old ` A ) u. ( _N ` A ) ) )

Proof

Step Hyp Ref Expression
1 madeoldsuc 
 |-  ( A e. On -> ( _M ` A ) = ( _Old ` suc A ) )
2 madeun 
 |-  ( A e. On -> ( _M ` A ) = ( ( _Old ` A ) u. ( _N ` A ) ) )
3 1 2 eqtr3d 
 |-  ( A e. On -> ( _Old ` suc A ) = ( ( _Old ` A ) u. ( _N ` A ) ) )