Theorem newval

Description: The value of the new options function. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	newval	|- ( A e. On -> ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( x = A -> ( _M ` x ) = ( _M ` A ) )
2		fveq2	|- ( x = A -> ( _Old ` x ) = ( _Old ` A ) )
3	1 2	difeq12d	|- ( x = A -> ( ( _M ` x ) \ ( _Old ` x ) ) = ( ( _M ` A ) \ ( _Old ` A ) ) )
4		df-new	|- _N = ( x e. On |-> ( ( _M ` x ) \ ( _Old ` x ) ) )
5		fvex	|- ( _M ` A ) e. _V
6	5	difexi	|- ( ( _M ` A ) \ ( _Old ` A ) ) e. _V
7	3 4 6	fvmpt	|- ( A e. On -> ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) ) )