Theorem oldsuc

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

	Ref	Expression
Assertion	oldsuc	Could not format assertion : No typesetting found for |- ( A e. On -> ( _Old ` suc A ) = ( ( _Old ` A ) u. ( _New ` A ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		madeoldsuc	Could not format ( A e. On -> ( _Made ` A ) = ( _Old ` suc A ) ) : No typesetting found for |- ( A e. On -> ( _Made ` A ) = ( _Old ` suc A ) ) with typecode |-
2		madeun	Could not format ( _Made ` A ) = ( ( _Old ` A ) u. ( _New ` A ) ) : No typesetting found for |- ( _Made ` A ) = ( ( _Old ` A ) u. ( _New ` A ) ) with typecode |-
3	1 2	eqtr3di	Could not format ( A e. On -> ( _Old ` suc A ) = ( ( _Old ` A ) u. ( _New ` A ) ) ) : No typesetting found for |- ( A e. On -> ( _Old ` suc A ) = ( ( _Old ` A ) u. ( _New ` A ) ) ) with typecode |-